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

J. C. Bradfield

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 33, Issue: 4-5, page 341-356
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

Bradfield, J. C.. "Fixpoint alternation: arithmetic, transition systems, and the binary tree." RAIRO - Theoretical Informatics and Applications 33.4-5 (2010): 341-356. <http://eudml.org/doc/221964>.

@article{Bradfield2010,
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. },
author = {Bradfield, J. C.},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Fixpoints; mu-calculus; alternation; modal logic.; modal mu-calculus alternation hierarchy},
language = {eng},
month = {3},
number = {4-5},
pages = {341-356},
publisher = {EDP Sciences},
title = {Fixpoint alternation: arithmetic, transition systems, and the binary tree},
url = {http://eudml.org/doc/221964},
volume = {33},
year = {2010},
}

TY - JOUR
AU - Bradfield, J. C.
TI - Fixpoint alternation: arithmetic, transition systems, and the binary tree
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 4-5
SP - 341
EP - 356
AB - 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.
LA - eng
KW - Fixpoints; mu-calculus; alternation; modal logic.; modal mu-calculus alternation hierarchy
UR - http://eudml.org/doc/221964
ER -

References

top
  1. A. Arnold, The µ-calculus alternation-depth hierarchy is strict on binary trees, this volume, p. 329.  
  2. J.C. Bradfield, Verifying Temporal Properties of Systems. Birkhäuser, Boston (1991).  
  3. 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.  
  4. J.C. Bradfield, The modal mu-calculus alternation hierarchy is strict. Theoret. Comput. Sci.195 (1997) 133-153.  
  5. 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.  
  6. J.C. Bradfield, Fixpoint alternation on the binary tree, Workshop on Fixpoints in Computer Science (FICS). Brno (1998).  
  7. E.A. Emerson and C.S. Jutla, Tree automata, mu-calculus and determinacy, in Proc. FOCS 91 (1991).  
  8. 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.  
  9. D. Janin and I. Walukiewicz, Automata for the µ-calculus and related results, in Proc. MFCS '95. Springer, Berlin, Lecture Notes in Comput. Sci.969 (1995) 552-562.  
  10. R. Kaye, Models of Peano Arithmetic. Oxford University Press, Oxford (1991).  
  11. D. Kozen, Results on the propositional mu-calculus. Theoret. Comput. Sci.27 (1983) 333-354.  
  12. G. Lenzi, 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.  
  13. R.S. Lubarsky, µ-definable sets of integers, J. Symbolic Logic58 (1993) 291-313.  
  14. D. Niwinski, On fixed point clones, L. Kott, Ed., in Proc. 13th ICALP. Springer, Berlin, Lecture Notes in Comput. Sci.226 (1986) 464-473.  
  15. D. Niwinski, Fixed point characterization of infinite behavior of finite state systems. Theoret. Comput. Sci.189 (1997) 1-69.  
  16. C.P. Stirling, Modal and temporal logics, S. Abramsky, D. Gabbay and T. Maibaum, Eds. Oxford University Press, Handb. Log. Comput. Sci.2 (1991) 477-563.  
  17. I. Walukiewicz, 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.  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.