TU Darmstadt Mathematik Fachgebiete Logic group Research Algorithmic Model Theory Boundedness Issues

Relational least fixed-point recursion provides an important extension beyond first-order logic. A key decision issue in connection with fixed-point recursions is the question whether they are bounded in the sense of admitting a fixed finite bound on their iteration depth. This problem seems to be decidable for only a very limited number of natural classes of formulae and/or over only very restricted classes of structures. One long-term goal in this direction is a classification of formula classes that have a decidable boundedness problem. Recent progress on decidability was made in [O06] and in [KOS07], where the boundedness problem was shown to be decidable for arbitrary monadic first-order recursions in restriction to acyclic relational structures. Pursuing this shift in emphasis, entirely new methods were brought to bear in co-operation with Achim Blumensath and Mark Weyer in [BOW09] to show the boundedness problem decidable for arbitrary recursions in monadic second-order over finite linearly ordered monadic structures (word structures). Further work in this direction is hoped to yield generalisations of these new techniques to tree structures – a generalisation which would settle several (known and conjectured) classical boundedness issues for fragments of first-order logic in a uniform manner.

[O06] M. Otto, ** The Boundedness Problem for Monadic Universal First-Order Logic**, *Proceedings of 21st IEEE Symposium on Logic in Computer Science LICS 2006*, pp 37-46.

Abstract BibTeX entry

[KOS07] S. Kreutzer, M. Otto and N. Schweikardt. ** Boundedness of Monadic FO over Acyclic Structures,** *Proceedings of 34th International Colloquium on Automata, Languages and Programming ICALP 2007, LNCS 4596*, pp 571-582.

Abstract BibTeX entry

[BOW09] A. Blumensath, M. Otto and M. Weyer. ** Boundedness of Monadic Second-Order Logic over Finite Words,** *Proceedings of 36th International Colloquium on Automata, Languages and Programming ICALP 2009, LNCS 5556*, pp 67-78.

Abstract BibTeX entry