Issue |
RAIRO-Theor. Inf. Appl.
Volume 37, Number 4, October-December 2003
Fixed Points in Computer Science (FICS'02)
|
|
---|---|---|
Page(s) | 337 - 364 | |
DOI | https://doi.org/10.1051/ita:2003023 | |
Published online | 15 January 2004 |
Domain mu-calculus
Department of Electrical Engineering and Computer Science,
Case Western Reserve University,
Cleveland, OH 44106, USA.;
gqz@eecs.cwru.edu.
Received:
30
October
2002
Accepted:
25
September
2003
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.
Mathematics Subject Classification: 03B70 / 68Q45 / 68Q55
Key words: Domain theory / mu-calculus / formal languages / Boolean automata.
© EDP Sciences, 2003
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.