Domain mu-calculus

Guo-Qiang Zhang

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2003)

  • Volume: 37, Issue: 4, page 337-364
  • ISSN: 0988-3754

Abstract

top
The basic framework of domain μ -calculus was formulated in [39] more than ten years ago. This paper provides an improved formulation of a fragment of the μ -calculus without function space or powerdomain constructions, and studies some open problems related to this μ -calculus such as decidability and expressive power. A class of language equations is introduced for encoding μ -formulas in order to derive results related to decidability and expressive power of non-trivial fragments of the domain μ -calculus. The existence and uniqueness of solutions to this class of language equations constitute an important component of this approach. Our formulation is based on the recent work of Leiss [23], who established a sophisticated framework for solving language equations using Boolean automata (a.k.a. alternating automata [12, 35]) and a generalized notion of language derivatives. Additionally, the early notion of even-linear grammars is adopted here to treat another fragment of the domain μ -calculus.

How to cite

top

Zhang, Guo-Qiang. "Domain mu-calculus." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 37.4 (2003): 337-364. <http://eudml.org/doc/244898>.

@article{Zhang2003,
abstract = {The basic framework of domain $\mu $-calculus was formulated in [39] more than ten years ago. This paper provides an improved formulation of a fragment of the $\mu $-calculus without function space or powerdomain constructions, and studies some open problems related to this $\mu $-calculus such as decidability and expressive power. A class of language equations is introduced for encoding $\mu $-formulas in order to derive results related to decidability and expressive power of non-trivial fragments of the domain $\mu $-calculus. The existence and uniqueness of solutions to this class of language equations constitute an important component of this approach. Our formulation is based on the recent work of Leiss [23], who established a sophisticated framework for solving language equations using Boolean automata (a.k.a. alternating automata [12, 35]) and a generalized notion of language derivatives. Additionally, the early notion of even-linear grammars is adopted here to treat another fragment of the domain $\mu $-calculus.},
author = {Zhang, Guo-Qiang},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {domain theory; mu-calculus; formal languages; boolean automata; domain -calculus; decidability; expressive power; language equations},
language = {eng},
number = {4},
pages = {337-364},
publisher = {EDP-Sciences},
title = {Domain mu-calculus},
url = {http://eudml.org/doc/244898},
volume = {37},
year = {2003},
}

TY - JOUR
AU - Zhang, Guo-Qiang
TI - Domain mu-calculus
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2003
PB - EDP-Sciences
VL - 37
IS - 4
SP - 337
EP - 364
AB - The basic framework of domain $\mu $-calculus was formulated in [39] more than ten years ago. This paper provides an improved formulation of a fragment of the $\mu $-calculus without function space or powerdomain constructions, and studies some open problems related to this $\mu $-calculus such as decidability and expressive power. A class of language equations is introduced for encoding $\mu $-formulas in order to derive results related to decidability and expressive power of non-trivial fragments of the domain $\mu $-calculus. The existence and uniqueness of solutions to this class of language equations constitute an important component of this approach. Our formulation is based on the recent work of Leiss [23], who established a sophisticated framework for solving language equations using Boolean automata (a.k.a. alternating automata [12, 35]) and a generalized notion of language derivatives. Additionally, the early notion of even-linear grammars is adopted here to treat another fragment of the domain $\mu $-calculus.
LA - eng
KW - domain theory; mu-calculus; formal languages; boolean automata; domain -calculus; decidability; expressive power; language equations
UR - http://eudml.org/doc/244898
ER -

References

top
  1. [1] S. Abramsky, Domain theory in logical form. Ann. Pure Appl. Logic 51 (1991) 1-77. Zbl0737.03006MR1100496
  2. [2] S. Abramsky and A. Jung, Domain theory. Clarendon Press, Handb. Log. Comput. Sci. 3 (1995) 1-168. MR1365749
  3. [3] S. Abramsky, A domain equation for bisimulation. Inf. Comput. 92 (1991) 161-218. Zbl0718.68057MR1109402
  4. [4] A. Arnold, The mu-calculus alternation-depth hierarchy is strict on binary trees. RAIRO Theoret. Informatics Appl. 33 (1999) 329-339. Zbl0945.68118MR1748659
  5. [5] V. Amar and G. Putzolu, On a family of linear grammars. Inf. Control 7 (1964) 283-291. Zbl0139.00703MR168399
  6. [6] V. Amar and G. Putzolu, Generalizations of regular events. Inf. Control 8 (1965) 56-63. Zbl0236.94041MR176856
  7. [7] S. Bloom and Z. Ésik, Equational axioms for regular sets. Technical Report 9101, Stevens Institute of Technology (1991). Zbl0796.68153
  8. [8] M. Bonsangue and J.N. Kok, Towards an infinitary logic of domains: Abramsky logic for transition systems. Inf. Comput. 155 (1999) 170-201. Zbl1004.03030MR1744248
  9. [9] J.C. Bradfield, Simplifying the modal mu-calculus alternation hierarchy. Lecture Notes in Comput. Sci. 1373 (1998) 39-49. Zbl0892.03005MR1650761
  10. [10] S. Brookes, A semantically based proof system for partial correctness and deadlock in CSP, in Proceedings, Symposium on Logic in Computer Science. Cambridge, Massachusetts (1986) 58-65. 
  11. [11] J. Brzozowski and E. Leiss, On equations for regular languages, finite automata, and sequential networks. Theor. Comput. Sci. 10 (1980) 19-35. Zbl0415.68023MR549752
  12. [12] A.K. Chandra, D. Kozen and L. Stockmyer, Alternation. Journal of the ACM 28 (1981) 114-133. Zbl0473.68043MR603186
  13. [13] Z. Ésik, Completeness of Park induction. Theor. Comput. Sci. 177 (1997) 217-283 (MFPS’94). Zbl0901.68107
  14. [14] A. Fellah, Alternating finite automata and related problems. Ph.D. thesis, Department of Mathematics and Computer Science, Kent State University (1991). 
  15. [15] A. Fellah, H. Jurgensen and S. Yu, Constructions for alternating finite automata. Int. J. Comput. Math. 35 (1990) 117-132. Zbl0699.68081
  16. [16] C. Gunter and D. Scott, Semantic domains. Jan van Leeuwen edn., Elsevier, Handb. Theoretical Comput. Sci. B (1990) 633-674. Zbl0900.68301MR1127197
  17. [17] D. Janin and I. Walukiewicz, On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. Lecture Notes in Comput. Sci. (CONCUR’96) 1119 (1996) 263-277. 
  18. [18] T. Jensen, Disjunctive program analysis for algebraic data types. ACM Trans. Programming Languages and Systems 19 (1997) 752-804. 
  19. [19] P.T. Johnstone, Stone Spaces. Cambridge University Press (1982). Zbl0499.54001MR698074
  20. [20] D. Kozen, Results on the propositional mu-calculus. Theor. Comput. Sci. 27 (1983) 333-354. Zbl0553.03007MR731069
  21. [21] D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110 (1994) 366-390. Zbl0806.68082MR1276741
  22. [22] E. Leiss, Succinct representation of regular languages by Boolean automata. Theor. Comput. Sci. 13 (1981) 323-330. Zbl0458.68017MR603263
  23. [23] E. Leiss, Language Equations. Monographs in Computer Science, Springer-Verlag, New York (1999). Zbl0926.68064MR1724110
  24. [24] R.S. Lubarsky, μ -definable sets of integers. J. Symb. Log. 58 (1993) 291-313. Zbl0776.03022MR1217190
  25. [25] D. Niwiński, Fixed points vs. infinite generation. IEEE Computer Press Logic in Computer Science (1988) 402-409. 
  26. [26] D. Niwiński, Fixed point characterization of infinite behaviour of finite state systems. Theor. Comput. Sci. 189 (1997) 1-69. Zbl0893.68102MR1483617
  27. [27] A. Okhotin, Automaton representation of linear conjunctive languages. Proceedings of DLT 2002, Lecture Notes in Comput. Sci. 2450 (2003) 393-404. Zbl1015.68093MR2177362
  28. [28] A. Okhotin, On the closure properties of linear conjunctive languages. Theor. Comput. Sci. 299 (2003) 663-685. Zbl1042.68069MR1973171
  29. [29] D. Park, Concurrency and automata on infinite sequences. Lecture Notes in Comput. Sci. 154 (1981) 561-572. Zbl0457.68049
  30. [30] G. Plotkin, The Pisa Notes. Department of Computer Science, University of Edinburgh (1981). 
  31. [31] G. Plotkin, A powerdomain construction. SIAM J. Computing 5 (1976) 452-487. Zbl0355.68015MR445891
  32. [32] V.R. Pratt, A decidable mu-calculus: Preliminary report, Proc. of IEEE 22nd Annual Symposium on Foundations of Computer Science (1981) 421-427. 
  33. [33] M. Presburger, On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operator. Hist. Philos. Logic 12 (1991) 225-233 (English translation of the original paper in 1930). Zbl0741.03027MR1111343
  34. [34] M.O. Rabin and D. Scott, Finite automata and their decision problems. IBM J. Res. 3 (1959) 115-125. Zbl0158.25404MR103795
  35. [35] M.Y. Vardi, Alternating automata and program verification. Computer Science Today – Recent Trends and Developments, Lecture Notes in Comput. Sci. 1000 (1995) 471-485. 
  36. [36] I. Walukiewicz, Completeness of Kozen’s axiomatisation of the propositional μ -calculus. Inf. Comput. 157 (2000) 142-182. Zbl1046.68628
  37. [37] G. Winskel, The Formal Semantics of Programming Languages. MIT Press (1993). Zbl0919.68082MR1219956
  38. [38] S. Yu, Regular Languages. Handbook of Formal Languages, Rozenberg and Salomaa, Springer-Verlag (1997) 41-110. MR1469994
  39. [39] G.-Q. Zhang, Logic of Domains. Birkhauser, Boston (1991). Zbl0854.68058MR1129241

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.