Domain mu-calculus

Zhang, Guo-Qiang

doi:10.1051/ita:2003023

Domain mu-calculus

Zhang, Guo-Qiang

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 337-364.

Résumé

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.

MR Zbl

DOI : 10.1051/ita:2003023

Classification : 03B70, 68Q45, 68Q55
Mots clés : domain theory, mu-calculus, formal languages, boolean automata

@article{ITA_2003__37_4_337_0,
     author = {Zhang, Guo-Qiang},
     title = {Domain mu-calculus},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {337--364},
     publisher = {EDP-Sciences},
     volume = {37},
     number = {4},
     year = {2003},
     doi = {10.1051/ita:2003023},
     mrnumber = {2053031},
     zbl = {1038.03038},
     language = {en},
     url = {http://archive.numdam.org/articles/10.1051/ita:2003023/}
}

TY  - JOUR
AU  - Zhang, Guo-Qiang
TI  - Domain mu-calculus
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2003
SP  - 337
EP  - 364
VL  - 37
IS  - 4
PB  - EDP-Sciences
UR  - http://archive.numdam.org/articles/10.1051/ita:2003023/
DO  - 10.1051/ita:2003023
LA  - en
ID  - ITA_2003__37_4_337_0
ER  -

%0 Journal Article
%A Zhang, Guo-Qiang
%T Domain mu-calculus
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2003
%P 337-364
%V 37
%N 4
%I EDP-Sciences
%U http://archive.numdam.org/articles/10.1051/ita:2003023/
%R 10.1051/ita:2003023
%G en
%F ITA_2003__37_4_337_0

Zhang, Guo-Qiang. Domain mu-calculus. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 37 (2003) no. 4, pp. 337-364. doi : 10.1051/ita:2003023. http://archive.numdam.org/articles/10.1051/ita:2003023/

Bibliographie
Cité par

[1] S. Abramsky, Domain theory in logical form. Ann. Pure Appl. Logic 51 (1991) 1-77. | MR | Zbl

[2] S. Abramsky and A. Jung, Domain theory. Clarendon Press, Handb. Log. Comput. Sci. 3 (1995) 1-168. | MR

[3] S. Abramsky, A domain equation for bisimulation. Inf. Comput. 92 (1991) 161-218. | MR | Zbl

[4] A. Arnold, The mu-calculus alternation-depth hierarchy is strict on binary trees. RAIRO Theoret. Informatics Appl. 33 (1999) 329-339. | Numdam | MR | Zbl

[5] V. Amar and G. Putzolu, On a family of linear grammars. Inf. Control 7 (1964) 283-291. | MR | Zbl

[6] V. Amar and G. Putzolu, Generalizations of regular events. Inf. Control 8 (1965) 56-63. | MR | Zbl

[7] S. Bloom and Z. Ésik, Equational axioms for regular sets. Technical Report 9101, Stevens Institute of Technology (1991). | Zbl

[8] M. Bonsangue and J.N. Kok, Towards an infinitary logic of domains: Abramsky logic for transition systems. Inf. Comput. 155 (1999) 170-201. | MR | Zbl

[9] J.C. Bradfield, Simplifying the modal mu-calculus alternation hierarchy. Lecture Notes in Comput. Sci. 1373 (1998) 39-49. | MR | Zbl

[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. | MR | Zbl

[12] A.K. Chandra, D. Kozen and L. Stockmyer, Alternation. Journal of the ACM 28 (1981) 114-133. | MR | Zbl

[13] Z. Ésik, Completeness of Park induction. Theor. Comput. Sci. 177 (1997) 217-283 (MFPS'94). | Zbl

[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. | Zbl

[16] C. Gunter and D. Scott, Semantic domains. Jan van Leeuwen edn., Elsevier, Handb. Theoretical Comput. Sci. B (1990) 633-674. | MR | Zbl

[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). | MR | Zbl

[20] D. Kozen, Results on the propositional mu-calculus. Theor. Comput. Sci. 27 (1983) 333-354. | MR | Zbl

[21] D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110 (1994) 366-390. | MR | Zbl

[22] E. Leiss, Succinct representation of regular languages by Boolean automata. Theor. Comput. Sci. 13 (1981) 323-330. | MR | Zbl

[23] E. Leiss, Language Equations. Monographs in Computer Science, Springer-Verlag, New York (1999). | MR | Zbl

[24] R.S. Lubarsky, $μ$ -definable sets of integers. J. Symb. Log. 58 (1993) 291-313. | MR | Zbl

[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. | MR | Zbl

[27] A. Okhotin, Automaton representation of linear conjunctive languages. Proceedings of DLT 2002, Lecture Notes in Comput. Sci. 2450 (2003) 393-404. | MR | Zbl

[28] A. Okhotin, On the closure properties of linear conjunctive languages. Theor. Comput. Sci. 299 (2003) 663-685. | MR | Zbl

[29] D. Park, Concurrency and automata on infinite sequences. Lecture Notes in Comput. Sci. 154 (1981) 561-572. | Zbl

[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. | MR | Zbl

[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). | MR | Zbl

[34] M.O. Rabin and D. Scott, Finite automata and their decision problems. IBM J. Res. 3 (1959) 115-125. | MR | Zbl

[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 $μ$ -calculus. Inf. Comput. 157 (2000) 142-182. | Zbl

[37] G. Winskel, The Formal Semantics of Programming Languages. MIT Press (1993). | MR | Zbl

[38] S. Yu, Regular Languages. Handbook of Formal Languages, Rozenberg and Salomaa, Springer-Verlag (1997) 41-110. | MR

[39] G.-Q. Zhang, Logic of Domains. Birkhauser, Boston (1991). | MR | Zbl

Cité par Sources :