The modal mu-calculus: a survey

• Autorzy: Lenzi G.
• Języki publikacji: EN

Abstrakty

EN

The modal mu-calculus is an extension of modal logic with two operators mu and ni, which give the least and greatest fixpoints of monotone operators on powersets. This powerful logic is widely used in computer science, in the area of verification of correctness of concurrent systems. In this survey we review both the theoretical aspects of the modal mu-calculus and its applications to computer science.

Słowa kluczowe

EN

mu-calculus; fixed points; model checking

• Wydawca: Politechnika Gdańska
• Czasopismo: TASK Quarterly : scientific bulletin of Academic Computer Centre in Gdansk
• Rocznik: 2005
• Tom: Vol. 9, No 3
• Strony: 293--316
• Opis fizyczny: Bibliogr. 48 poz.

Twórcy

autor

Lenzi G.

• University of Pisa, Department of Mathematics, Largo Pontecorvo 5, 56127 Pisa, Italy,

Bibliografia

• [1] Kozen D 1983 Theoret. Comput. Sci. 27 333
• [2] Arnold A and Niwiński D 2001 Rudiments of µ-calculus, North-Holland
• [3] Janin D and Walukiewicz I 1996 Proc. CONCUR ’96, Lecture Notes in Comput. Sci. 1119 263
• [4] Emerson A and Jutla C 1988 Proc. of IEEE FOCS, Piscataway, USA, pp. 328–337
• [5] Emerson A 1997 Proc. of the DIMACS Symp. on Descriptive Complexity and Finite Models, AMS Press, pp. 185–214
• [6] Lenzi G 1997 The µ-Calculus and the Hierarchy Problem, PhD Thesis, Scuola Normale Superiore, Pisa
• [7] Bradfield J and Stirling C 2001 Modal Logics and µ-Calculi: an Introduction, in: Handbook of Process Algebra, Elsevier, Chap. 4, pp. 293–330
• [8] Dam M 1994 Theoret. Comput. Sci. 126 77
• [9] Pnueli A 1977 Proc. 18 th IEEE FOCS, Providence, USA, pp. 46–57
• [10] Clarke E and Emerson A 1982 Proc. of the Workshop on Logics of Programs, Lecture Notes in Comput. Sci. 131 52
• [11] Emerson A and Halpern J 1986 J. of the ACM 33 (1) 151
• [12] Pratt V 1976 Proc. of FOCS ’76, Houston, USA, pp. 109–121
• [13] Streett R and Emerson A 1989 Inform. and Comput. 81 249
• [14] Stirling C and Walker D 1991 Theoret. Comput. Sci. 89 161
• [15] Bradfield J 1991 Verifying Temporal Properties of Systems, Birkh¨auser
• [16] Bradfield J and Stirling C 1992 Theoret. Comput. Sci. 96 157
• [17] Walukiewicz I 1995 Proc. 10 th IEEE LICS, San Diego, USA, pp. 14–24
• [18] Janin D and Walukiewicz I 1995 Proc. MFCS ’95, Lecture Notes in Comput. Sci. 969 552
• [19] Walukiewicz I 1995 BRICS Notes Series 95-1, http://www.brics.dk/BRICS/NS/95/1/BRICS-NS-95-1/index.html
• [20] Emerson A and Lei C 1986 Proc. 1 st IEEE LICS, Cambridge, USA, pp. 267–278
• [21] Niwiński D 1986 Proc. ICALP ’86, Lecture Notes in Comput. Sci. 226 464
• [22] Arnold A and Niwiński D 1990 J. Inform. Process. Cybernet. EIK 26 451
• [23] Bradfield J 1997 Theoret. Comput. Sci. 195 133
• [24] Lenzi G 1996 Proc. ICALP ’96, Lecture Notes in Comput. Sci. 1099 87
• [25] Bradfield J 1998 Proc. STACS ’98, Lecture Notes in Comp. Sci. 1373 39
• [26] Arnold A 1999 RAIRO-Theoretical Informatics and Applications 33 329
• [27] Janin D and Lenzi G 2001 Proc. of LICS, Boston, USA, pp. 347–356
• [28] Janin D and Lenzi G 2002 Computing and Informatics 21 185
• [29] Janin D and Lenzi G 2004 Fund. Inform. 61 (3-4) 247
• [30] van Benthem J 1976 Modal Correspondence Theory, PhD Thesis, University of Amsterdam
• [31] Rosen E 1997 J. of Logic, Language and Computation 6 (4) 427
• [32] Thomas W 1998 Languages, Automata and Logic. Handbook of Formal Language Theory, vol. III, Springer-Verlag, New York, pp. 389-455
• [33] Niwiński D 1997 Theoret. Comput. Sci. 189 1
• [34] Rabin M 1969 Trans. Amer. Math. Soc. 141 1
• [35] Emerson A 1981 Branching Time Temporal Logics and the Design of Correct Concurrent Programs, PhD Thesis, Division of Applied Sciences, Harvard University
• [36] Queille J and Sifakis J 1982 Proc. 5 th Int. Symp. Prog., Lecture Notes in Comput. Sci. 137 195
• [37] Clarke E, Emerson A and Sistla P 1983 10 th ACM Symp. on Principles of Prog. Lang.; journal version: 1986 ACM Trans. on Prog. Lang. and Sys. 8 (2) 244
• [38] Stirling C and Walker D 1989 Lecture Notes in Comput. Sci. 351 369
• [39] Jard C and Jeron T 1989 Int. Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Comput. Sci. 407 189
• [40] Lichtenstein O and Pnueli A 1985 Proc. of POPL ’85, New Orleans, USA, pp. 97–107
• [41] Emerson A, Jutla C and Sistla P 1993 Proc. CAV ’93, Lecture Notes in Comput. Sci. 697 385
• [42] Jurdzinski M 1998 Inf. Process. Lett. 68 119
• [43] McMillan K 1992 Symbolic Model Checking: an Approach to the State Explosion Problem, PhD Thesis, Carnegie-Mellon University
• [44] Burch J, Clarke E, McMillan M, Dill D and Hwang L 1990 Proc. of the 5 th Annual IEEE-CS Symposium on Logic in Computer Science, Philadelphia, USA, pp. 428–439
• [45] Pixley C 1990 CAV ’90 DIMACS series 3 (also DIMACS Tech. Report 90-31)
• [46] Coudert O and Madre J 1990 Computer Aided Verification ’90, DIMACS Series, pp. 75–84
• [47] Bryant R 1986 IEEE Trans. on Computers C-35 (8) 677
• [48] Galperin H and Wigderson A 1983 Information and Control 56 183