# Domain mu-calculus

RAIRO - Theoretical Informatics and Applications (2010)

- 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 37.4 (2010): 337-364. <http://eudml.org/doc/92727>.

@article{Zhang2010,

abstract = {
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.
},

author = {Zhang, Guo-Qiang},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Domain theory; mu-calculus; formal languages; Boolean automata.},

language = {eng},

month = {3},

number = {4},

pages = {337-364},

publisher = {EDP Sciences},

title = {Domain mu-calculus},

url = {http://eudml.org/doc/92727},

volume = {37},

year = {2010},

}

TY - JOUR

AU - Zhang, Guo-Qiang

TI - Domain mu-calculus

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 37

IS - 4

SP - 337

EP - 364

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

LA - eng

KW - Domain theory; mu-calculus; formal languages; Boolean automata.

UR - http://eudml.org/doc/92727

ER -

## References

top- S. Abramsky, Domain theory in logical form. Ann. Pure Appl. Logic51 (1991) 1-77 . Zbl0737.03006
- S. Abramsky and A. Jung, Domain theory. Clarendon Press, Handb. Log. Comput. Sci. 3 (1995) 1-168.
- S. Abramsky, A domain equation for bisimulation. Inf. Comput.92 (1991) 161-218. Zbl0718.68057
- A. Arnold, The mu-calculus alternation-depth hierarchy is strict on binary trees. RAIRO Theoret. Informatics Appl.33 (1999) 329-339. Zbl0945.68118
- V. Amar and G. Putzolu, On a family of linear grammars. Inf. Control7 (1964) 283-291. Zbl0139.00703
- V. Amar and G. Putzolu, Generalizations of regular events. Inf. Control8 (1965) 56-63. Zbl0236.94041
- S. Bloom and Z. Ésik, Equational axioms for regular sets. Technical Report 9101, Stevens Institute of Technology (1991). Zbl0796.68153
- M. Bonsangue and J.N. Kok, Towards an infinitary logic of domains: Abramsky logic for transition systems. Inf. Comput.155 (1999) 170-201. Zbl1004.03030
- J.C. Bradfield, Simplifying the modal mu-calculus alternation hierarchy. Lecture Notes in Comput. Sci.1373 (1998) 39-49. Zbl0892.03005
- 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.
- J. Brzozowski and E. Leiss, On equations for regular languages, finite automata, and sequential networks. Theor. Comput. Sci.10 (1980) 19-35 . Zbl0415.68023
- A.K. Chandra, D. Kozen and L. Stockmyer, Alternation. Journal of the ACM28 (1981) 114-133 .
- Z. Ésik, Completeness of Park induction. Theor. Comput. Sci.177 (1997) 217-283 (MFPS'94). Zbl0901.68107
- A. Fellah, Alternating finite automata and related problems. Ph.D. thesis, Department of Mathematics and Computer Science, Kent State University (1991).
- A. Fellah, H. Jurgensen and S. Yu, Constructions for alternating finite automata. Int. J. Comput. Math.35 (1990) 117-132. Zbl0699.68081
- C. Gunter and D. Scott, Semantic domains. Jan van Leeuwen edn., Elsevier, Handb. Theoretical Comput. Sci.B (1990) 633-674. Zbl0900.68301
- 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.
- T. Jensen, Disjunctive program analysis for algebraic data types. ACM Trans. Programming Languages and Systems19 (1997) 752-804.
- P.T. Johnstone, Stone Spaces. Cambridge University Press (1982).
- D. Kozen, Results on the propositional mu-calculus. Theor. Comput. Sci.27 (1983) 333-354 . Zbl0553.03007
- D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput.110 (1994) 366-390. Zbl0806.68082
- E. Leiss, Succinct representation of regular languages by Boolean automata. Theor. Comput. Sci.13 (1981) 323-330. Zbl0458.68017
- E. Leiss, Language Equations. Monographs in Computer Science, Springer-Verlag, New York (1999).
- R.S. Lubarsky, μ-definable sets of integers. J. Symb. Log.58 (1993) 291-313. Zbl0776.03022
- D. Niwinski, Fixed points vs. infinite generation. IEEE Computer Press Logic in Computer Science (1988) 402-409.
- D. Niwinski, Fixed point characterization of infinite behaviour of finite state systems. Theor. Comput. Sci.189 (1997) 1-69 . Zbl0893.68102
- A. Okhotin, Automaton representation of linear conjunctive languages. Proceedings of DLT 2002, Lecture Notes in Comput. Sci.2450 (2003) 393-404. Zbl1015.68093
- A. Okhotin, On the closure properties of linear conjunctive languages. Theor. Comput. Sci.299 (2003) 663-685 . Zbl1042.68069
- D. Park, Concurrency and automata on infinite sequences. Lecture Notes in Comput. Sci.154 (1981) 561-572.
- G. Plotkin, The Pisa Notes. Department of Computer Science, University of Edinburgh (1981).
- G. Plotkin, A powerdomain construction. SIAM J. Computing5 (1976) 452-487. Zbl0355.68015
- V.R. Pratt, A decidable mu-calculus: Preliminary report, Proc. of IEEE 22nd Annual Symposium on Foundations of Computer Science (1981) 421-427.
- M. Presburger, On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operator. Hist. Philos. Logic12 (1991) 225-233 (English translation of the original paper in 1930). Zbl0741.03027
- M.O. Rabin and D. Scott, Finite automata and their decision problems. IBM J. Res.3 (1959) 115-125. Zbl0158.25404
- M.Y. Vardi, Alternating automata and program verification. Computer Science Today - Recent Trends and Developments, Lecture Notes in Comput. Sci.1000 (1995) 471-485.
- I. Walukiewicz, Completeness of Kozen's axiomatisation of the propositional μ-calculus. Inf. Comput.157 (2000) 142-182. Zbl1046.68628
- G. Winskel, The Formal Semantics of Programming Languages. MIT Press (1993).
- S. Yu, Regular Languages. Handbook of Formal Languages, Rozenberg and Salomaa, Springer-Verlag (1997) 41-110.
- G.-Q. Zhang, Logic of Domains. Birkhauser, Boston (1991).

## NotesEmbed ?

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