12 Boundedness FP recursion

Algorithmic Model Theory


Boundedness Issues in Fixed-Point Recursion

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