Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-23T18:55:15.204Z Has data issue: false hasContentIssue false
  • English
  • Français

Fixpoint alternation: arithmetic, transition systems, and the binary tree

Published online by Cambridge University Press:  15 August 2002

J. C. Bradfield
J. C. Bradfield*
Affiliation:
LFCS, Division of Informatics, University of Edinburgh, Edinburgh EH9 3JZ, U.K., [email protected]. BRICS, Department of Computer Science, Aarhus University, Bygning 540, Ny Munkegade, 8000 Århus C, Denmark.
Get access

Abstract

We provide an elementary proof of the fixpoint alternation hierarchy in arithmetic, which in turn allows us to simplify the proof of the modal mu-calculus alternation hierarchy. We further show that the alternation hierarchy on the binary tree is strict, resolving a problem of Niwiński.

Keywords

Fixpointsmu-calculusalternationmodal logic.
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 33 , Issue 4-5 , July 1999 , pp. 341 - 356
Copyright
© EDP Sciences, 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

A. Arnold, The µ-calculus alternation-depth hierarchy is strict on binary trees, this volume, p. 329.
J.C. Bradfield, Verifying Temporal Properties of Systems. Birkhäuser, Boston (1991).
J.C. Bradfield, On the expressivity of the modal mu-calculus, C. Puech and R. Reischuk, Eds., in Proc. STACS '96. Springer, Berlin, Lecture Notes in Comput. Sci. 1046 (1996) 479-490.
Bradfield, J.C., The modal mu-calculus alternation hierarchy is strict. Theoret. Comput. Sci. 195 (1997) 133-153. CrossRef
J.C. Bradfield, Simplifying the modal mu-calculus alternation hierarchy, M. Morvan, C. Meinel and D. Krob, Eds., in Proc. STACS 98. Springer, Berlin, Lecture Notes in Comput. Sci. 1373 (1998) 39-49.
J.C. Bradfield, Fixpoint alternation on the binary tree, Workshop on Fixpoints in Computer Science (FICS). Brno (1998).
E.A. Emerson and C.S. Jutla, Tree automata, mu-calculus and determinacy, in Proc. FOCS 91 (1991).
E.A. Emerson and C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus, in Proc. 1st LICS. IEEE, Los Alamitos, CA (1986) 267-278.
Janin, D. and Walukiewicz, I., Automata for the µ-calculus and related results, in Proc. MFCS '95. Springer, Berlin, Lecture Notes in Comput. Sci. 969 (1995) 552-562. CrossRef
R. Kaye, Models of Peano Arithmetic. Oxford University Press, Oxford (1991).
Kozen, D., Results on the propositional mu-calculus. Theoret. Comput. Sci. 27 (1983) 333-354. CrossRef
Lenzi, G., A hierarchy theorem for the mu-calculus, F. Meyer auf der Heide and B. Monien, Eds., in Proc. ICALP '96. Springer, Berlin, Lecture Notes in Comput. Sci. 1099 (1996) 87-109. CrossRef
Lubarsky, R.S., µ-definable sets of integers, J. Symbolic Logic 58 (1993) 291-313. CrossRef
Niwinski, D., On fixed point clones, L. Kott, Ed., in Proc. 13th ICALP. Springer, Berlin, Lecture Notes in Comput. Sci. 226 (1986) 464-473. CrossRef
Niwinski, D., Fixed point characterization of infinite behavior of finite state systems. Theoret. Comput. Sci. 189 (1997) 1-69. CrossRef
Stirling, C.P., Modal and temporal logics, S. Abramsky, D. Gabbay and T. Maibaum, Eds. Oxford University Press, Handb. Log. Comput. Sci. 2 (1991) 477-563.
Walukiewicz, I., Monadic second order logic on tree-like structures, C. Puech and Rüdiger Reischuk, Eds., in Proc. STACS '96. Springer, Berlin, Lecture Notes in Comput. Sci. 1046 (1996) 401-414.