# Domain mu-calculus

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

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

## Access Full Article

top## Abstract

top## How to cite

topZhang, 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] S. Abramsky, Domain theory in logical form. Ann. Pure Appl. Logic 51 (1991) 1-77. Zbl0737.03006MR1100496
- [2] S. Abramsky and A. Jung, Domain theory. Clarendon Press, Handb. Log. Comput. Sci. 3 (1995) 1-168. MR1365749
- [3] S. Abramsky, A domain equation for bisimulation. Inf. Comput. 92 (1991) 161-218. Zbl0718.68057MR1109402
- [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] V. Amar and G. Putzolu, On a family of linear grammars. Inf. Control 7 (1964) 283-291. Zbl0139.00703MR168399
- [6] V. Amar and G. Putzolu, Generalizations of regular events. Inf. Control 8 (1965) 56-63. Zbl0236.94041MR176856
- [7] S. Bloom and Z. Ésik, Equational axioms for regular sets. Technical Report 9101, Stevens Institute of Technology (1991). Zbl0796.68153
- [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] J.C. Bradfield, Simplifying the modal mu-calculus alternation hierarchy. Lecture Notes in Comput. Sci. 1373 (1998) 39-49. Zbl0892.03005MR1650761
- [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] 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] A.K. Chandra, D. Kozen and L. Stockmyer, Alternation. Journal of the ACM 28 (1981) 114-133. Zbl0473.68043MR603186
- [13] Z. Ésik, Completeness of Park induction. Theor. Comput. Sci. 177 (1997) 217-283 (MFPS’94). Zbl0901.68107
- [14] A. Fellah, Alternating finite automata and related problems. Ph.D. thesis, Department of Mathematics and Computer Science, Kent State University (1991).
- [15] A. Fellah, H. Jurgensen and S. Yu, Constructions for alternating finite automata. Int. J. Comput. Math. 35 (1990) 117-132. Zbl0699.68081
- [16] C. Gunter and D. Scott, Semantic domains. Jan van Leeuwen edn., Elsevier, Handb. Theoretical Comput. Sci. B (1990) 633-674. Zbl0900.68301MR1127197
- [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] T. Jensen, Disjunctive program analysis for algebraic data types. ACM Trans. Programming Languages and Systems 19 (1997) 752-804.
- [19] P.T. Johnstone, Stone Spaces. Cambridge University Press (1982). Zbl0499.54001MR698074
- [20] D. Kozen, Results on the propositional mu-calculus. Theor. Comput. Sci. 27 (1983) 333-354. Zbl0553.03007MR731069
- [21] D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110 (1994) 366-390. Zbl0806.68082MR1276741
- [22] E. Leiss, Succinct representation of regular languages by Boolean automata. Theor. Comput. Sci. 13 (1981) 323-330. Zbl0458.68017MR603263
- [23] E. Leiss, Language Equations. Monographs in Computer Science, Springer-Verlag, New York (1999). Zbl0926.68064MR1724110
- [24] R.S. Lubarsky, $\mu $-definable sets of integers. J. Symb. Log. 58 (1993) 291-313. Zbl0776.03022MR1217190
- [25] D. Niwiński, Fixed points vs. infinite generation. IEEE Computer Press Logic in Computer Science (1988) 402-409.
- [26] D. Niwiński, Fixed point characterization of infinite behaviour of finite state systems. Theor. Comput. Sci. 189 (1997) 1-69. Zbl0893.68102MR1483617
- [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] A. Okhotin, On the closure properties of linear conjunctive languages. Theor. Comput. Sci. 299 (2003) 663-685. Zbl1042.68069MR1973171
- [29] D. Park, Concurrency and automata on infinite sequences. Lecture Notes in Comput. Sci. 154 (1981) 561-572. Zbl0457.68049
- [30] G. Plotkin, The Pisa Notes. Department of Computer Science, University of Edinburgh (1981).
- [31] G. Plotkin, A powerdomain construction. SIAM J. Computing 5 (1976) 452-487. Zbl0355.68015MR445891
- [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] 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] M.O. Rabin and D. Scott, Finite automata and their decision problems. IBM J. Res. 3 (1959) 115-125. Zbl0158.25404MR103795
- [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] I. Walukiewicz, Completeness of Kozen’s axiomatisation of the propositional $\mu $-calculus. Inf. Comput. 157 (2000) 142-182. Zbl1046.68628
- [37] G. Winskel, The Formal Semantics of Programming Languages. MIT Press (1993). Zbl0919.68082MR1219956
- [38] S. Yu, Regular Languages. Handbook of Formal Languages, Rozenberg and Salomaa, Springer-Verlag (1997) 41-110. MR1469994
- [39] G.-Q. Zhang, Logic of Domains. Birkhauser, Boston (1991). Zbl0854.68058MR1129241

## NotesEmbed ?

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