Domain \(\mu\)-calculus. (English) Zbl 1038.03038
Summary: The basic framework of domain \(\mu\)-calculus was formulated in the author’s monograph [Logic of domains. Basel: Birkhäuser (1991; Zbl 0854.68058)] 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 E. L. Leiss [Language equations. New York: Springer (1999; Zbl 0926.68064)], who established a sophisticated framework for solving language equations using Boolean automata (a.k.a. alternating automata) 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.
MSC:
| 03B70 | Logic in computer science |
| 68Q45 | Formal languages and automata |
| 68Q55 | Semantics in the theory of computing |
References:
| [1] | S. Abramsky , Domain theory in logical form . Ann. Pure Appl. Logic 51 ( 1991 ) 1 - 77 . MR 1100496 | Zbl 0737.03006 · Zbl 0737.03006 · doi:10.1016/0168-0072(91)90065-T |
| [2] | S. Abramsky and A. Jung , Domain theory . Clarendon Press, Handb. Log. Comput. Sci. 3 ( 1995 ) 1 - 168 . MR 1365749 |
| [3] | S. Abramsky , A domain equation for bisimulation . Inf. Comput. 92 ( 1991 ) 161 - 218 . MR 1109402 | Zbl 0718.68057 · Zbl 0718.68057 · doi:10.1006/inco.1991.9999 |
| [4] | A. Arnold , The mu-calculus alternation-depth hierarchy is strict on binary trees . RAIRO Theoret. Informatics Appl. 33 ( 1999 ) 329 - 339 . Numdam | MR 1748659 | Zbl 0945.68118 · Zbl 0945.68118 · doi:10.1051/ita:1999121 |
| [5] | V. Amar and G. Putzolu , On a family of linear grammars . Inf. Control 7 ( 1964 ) 283 - 291 . MR 168399 | Zbl 0139.00703 · Zbl 0139.00703 · doi:10.1016/S0019-9958(64)90294-3 |
| [6] | V. Amar and G. Putzolu , Generalizations of regular events . Inf. Control 8 ( 1965 ) 56 - 63 . MR 176856 | Zbl 0236.94041 · Zbl 0236.94041 · doi:10.1016/S0019-9958(65)90275-5 |
| [7] | S. Bloom and Z. Ésik , Equational axioms for regular sets . Technical Report 9101, Stevens Institute of Technology ( 1991 ). Zbl 0796.68153 · Zbl 0796.68153 · doi:10.1017/S0960129500000104 |
| [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 1744248 | Zbl 1004.03030 · Zbl 1004.03030 · doi:10.1006/inco.1999.2827 |
| [9] | J.C. Bradfield , Simplifying the modal mu-calculus alternation hierarchy . Lecture Notes in Comput. Sci. 1373 ( 1998 ) 39 - 49 . MR 1650761 | Zbl 0892.03005 · Zbl 0892.03005 |
| [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 549752 | Zbl 0415.68023 · Zbl 0415.68023 · doi:10.1016/0304-3975(80)90069-9 |
| [12] | A.K. Chandra , D. Kozen and L. Stockmyer , Alternation . Journal of the ACM 28 ( 1981 ) 114 - 133 . MR 603186 | Zbl 0473.68043 · Zbl 0473.68043 · doi:10.1145/322234.322243 |
| [13] | Z. Ésik , Completeness of Park induction . Theor. Comput. Sci. 177 ( 1997 ) 217 - 283 (MFPS’94). Zbl 0901.68107 · Zbl 0901.68107 · doi:10.1016/S0304-3975(96)00240-X |
| [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 0699.68081 · Zbl 0699.68081 · doi:10.1080/00207169008803893 |
| [16] | C. Gunter and D. Scott , Semantic domains . Jan van Leeuwen edn., Elsevier, Handb. Theoretical Comput. Sci. B ( 1990 ) 633 - 674 . MR 1127197 | Zbl 0900.68301 · Zbl 0900.68301 |
| [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 698074 | Zbl 0499.54001 · Zbl 0499.54001 |
| [20] | D. Kozen , Results on the propositional mu-calculus . Theor. Comput. Sci. 27 ( 1983 ) 333 - 354 . MR 731069 | Zbl 0553.03007 · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6 |
| [21] | D. Kozen , A completeness theorem for Kleene algebras and the algebra of regular events . Inf. Comput. 110 ( 1994 ) 366 - 390 . MR 1276741 | Zbl 0806.68082 · Zbl 0806.68082 · doi:10.1006/inco.1994.1037 |
| [22] | E. Leiss , Succinct representation of regular languages by Boolean automata . Theor. Comput. Sci. 13 ( 1981 ) 323 - 330 . MR 603263 | Zbl 0458.68017 · Zbl 0458.68017 · doi:10.1016/S0304-3975(81)80005-9 |
| [23] | E. Leiss , Language Equations . Monographs in Computer Science, Springer-Verlag, New York ( 1999 ). MR 1724110 | Zbl 0926.68064 · Zbl 0926.68064 |
| [24] | R.S. Lubarsky , \(\mu \)-definable sets of integers . J. Symb. Log. 58 ( 1993 ) 291 - 313 . Article | MR 1217190 | Zbl 0776.03022 · Zbl 0776.03022 · doi:10.2307/2275338 |
| [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 1483617 | Zbl 0893.68102 · Zbl 0893.68102 · doi:10.1016/S0304-3975(97)00039-X |
| [27] | A. Okhotin , Automaton representation of linear conjunctive languages . Proceedings of DLT 2002, Lecture Notes in Comput. Sci. 2450 ( 2003 ) 393 - 404 . MR 2177362 | Zbl 1015.68093 · Zbl 1015.68093 |
| [28] | A. Okhotin , On the closure properties of linear conjunctive languages . Theor. Comput. Sci. 299 ( 2003 ) 663 - 685 . MR 1973171 | Zbl 1042.68069 · Zbl 1042.68069 · doi:10.1016/S0304-3975(02)00543-1 |
| [29] | D. Park , Concurrency and automata on infinite sequences . Lecture Notes in Comput. Sci. 154 ( 1981 ) 561 - 572 . Zbl 0457.68049 · Zbl 0457.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 . MR 445891 | Zbl 0355.68015 · Zbl 0355.68015 · doi:10.1137/0205035 |
| [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 1111343 | Zbl 0741.03027 · Zbl 0741.03027 · doi:10.1080/014453409108837187 |
| [34] | M.O. Rabin and D. Scott , Finite automata and their decision problems . IBM J. Res. 3 ( 1959 ) 115 - 125 . MR 103795 | Zbl 0158.25404 · Zbl 0158.25404 |
| [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 . Zbl 1046.68628 · Zbl 1046.68628 · doi:10.1006/inco.1999.2836 |
| [37] | G. Winskel , The Formal Semantics of Programming Languages . MIT Press ( 1993 ). MR 1219956 | Zbl 0919.68082 · Zbl 0919.68082 |
| [38] | S. Yu , Regular Languages . Handbook of Formal Languages, Rozenberg and Salomaa, Springer-Verlag ( 1997 ) 41 - 110 . MR 1469994 |
| [39] | G.-Q. Zhang , Logic of Domains . Birkhauser, Boston ( 1991 ). MR 1129241 | Zbl 0854.68058 · Zbl 0854.68058 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
