Domain mu-calculus

Guo-Qiang Zhang

RAIRO - Theoretical Informatics and Applications (2010)

  • 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 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
  1. S. Abramsky, Domain theory in logical form. Ann. Pure Appl. Logic51 (1991) 1-77 .  
  2. S. Abramsky and A. Jung, Domain theory. Clarendon Press, Handb. Log. Comput. Sci. 3 (1995) 1-168.  
  3. S. Abramsky, A domain equation for bisimulation. Inf. Comput.92 (1991) 161-218.  
  4. A. Arnold, The mu-calculus alternation-depth hierarchy is strict on binary trees. RAIRO Theoret. Informatics Appl.33 (1999) 329-339.  
  5. V. Amar and G. Putzolu, On a family of linear grammars. Inf. Control7 (1964) 283-291.  
  6. V. Amar and G. Putzolu, Generalizations of regular events. Inf. Control8 (1965) 56-63.  
  7. S. Bloom and Z. Ésik, Equational axioms for regular sets. Technical Report 9101, Stevens Institute of Technology (1991).  
  8. M. Bonsangue and J.N. Kok, Towards an infinitary logic of domains: Abramsky logic for transition systems. Inf. Comput.155 (1999) 170-201.  
  9. J.C. Bradfield, Simplifying the modal mu-calculus alternation hierarchy. Lecture Notes in Comput. Sci.1373 (1998) 39-49.  
  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 .  
  12. A.K. Chandra, D. Kozen and L. Stockmyer, Alternation. Journal of the ACM28 (1981) 114-133 .  
  13. Z. Ésik, Completeness of Park induction. Theor. Comput. Sci.177 (1997) 217-283 (MFPS'94).  
  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.  
  16. C. Gunter and D. Scott, Semantic domains. Jan van Leeuwen edn., Elsevier, Handb. Theoretical Comput. Sci.B (1990) 633-674.  
  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 Systems19 (1997) 752-804.  
  19. P.T. Johnstone, Stone Spaces. Cambridge University Press (1982).  
  20. D. Kozen, Results on the propositional mu-calculus. Theor. Comput. Sci.27 (1983) 333-354 .  
  21. D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput.110 (1994) 366-390.  
  22. E. Leiss, Succinct representation of regular languages by Boolean automata. Theor. Comput. Sci.13 (1981) 323-330.  
  23. E. Leiss, Language Equations. Monographs in Computer Science, Springer-Verlag, New York (1999).  
  24. R.S. Lubarsky, μ-definable sets of integers. J. Symb. Log.58 (1993) 291-313.  
  25. D. Niwinski, Fixed points vs. infinite generation. IEEE Computer Press Logic in Computer Science (1988) 402-409.  
  26. D. Niwinski, Fixed point characterization of infinite behaviour of finite state systems. Theor. Comput. Sci.189 (1997) 1-69 .  
  27. A. Okhotin, Automaton representation of linear conjunctive languages. Proceedings of DLT 2002, Lecture Notes in Comput. Sci.2450 (2003) 393-404.  
  28. A. Okhotin, On the closure properties of linear conjunctive languages. Theor. Comput. Sci.299 (2003) 663-685 .  
  29. D. Park, Concurrency and automata on infinite sequences. Lecture Notes in Comput. Sci.154 (1981) 561-572.  
  30. G. Plotkin, The Pisa Notes. Department of Computer Science, University of Edinburgh (1981).  
  31. G. Plotkin, A powerdomain construction. SIAM J. Computing5 (1976) 452-487.  
  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. Logic12 (1991) 225-233 (English translation of the original paper in 1930).  
  34. M.O. Rabin and D. Scott, Finite automata and their decision problems. IBM J. Res.3 (1959) 115-125.  
  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.  
  37. G. Winskel, The Formal Semantics of Programming Languages. MIT Press (1993).  
  38. S. Yu, Regular Languages. Handbook of Formal Languages, Rozenberg and Salomaa, Springer-Verlag (1997) 41-110.  
  39. G.-Q. Zhang, Logic of Domains. Birkhauser, Boston (1991).  

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.