A note on negative tagging for least fixed-point formulae
Gurov, Dilian ; Kapron, Bruce
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 33 (1999), p. 383-392 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)
Publié le : 1999-01-01
@article{ITA_1999__33_4-5_383_0,
     author = {Gurov, Dilian and Kapron, Bruce},
     title = {A note on negative tagging for least fixed-point formulae},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     volume = {33},
     year = {1999},
     pages = {383-392},
     mrnumber = {1748662},
     zbl = {0940.03034},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ITA_1999__33_4-5_383_0}
}

Gurov, Dilian; Kapron, Bruce. A note on negative tagging for least fixed-point formulae. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 33 (1999) pp. 383-392. http://gdmltest.u-ga.fr/item/ITA_1999__33_4-5_383_0/

[1] H.R. Andersen, Verification of Temporal Properties of Concurrent Systems. Ph. D. Thesis, Computer Science Department, Aarhus University, Denmark (1993).

[2] H. R. Andersen, C. Stirling and G. Winskel, A compositional proof System for the modal mu-calculus, in Proc. of LICS'94 (1994).

[3] J. Bradfield, Verifying Temporal Properties of Systems. Birkhauser (1992). | Zbl 0753.68065

[4] M. Dam, CTL* and ECTL* as fragments of the modal μ-calculus. Theoret. Comput. Sci. 126 (1994) 77-96. | MR 1268023 | Zbl 0798.03018

[5] M. Dam, Proving properties of dynamic process networks. Inform. and Comput. 140 (1998) 95-114. | MR 1604188 | Zbl 0892.68034

[6] M. Dam, L. Fredlund and D. Gurov, Toward parametric verification of open distributed systems, H. Langmaack, A. Pnueli and W.-P. De Roever, Eds., Compositionality: The Significant Difference. Springer, Lecture Notes in Comput Sci. 1536 (1998) 150-158. | MR 1721664

[7] D. Gurov, S. Berezin and B. Kapron, A modal μ-calculus and a proof System for value passing processes. Electron. Notes Theoret. Comput. Sci. 5 (1996). | MR 1490312 | Zbl 0912.68185

[8] D. Kozen, Results on the propositional μ-calculus. Theoret. Comput. Sci. 27 (1983) 333-354. | MR 731069 | Zbl 0553.03007

[9] C. Stirling and D. Walker, Local model checking in the modal mu-calculus. Theoret. Comput. Sci. 89 (1991) 161-177. | MR 1133710 | Zbl 0745.03027

[10] R. S. Streett and E. A. Emerson, An automata theoretic decision procedure for the propositional mu-calculus. Inform. and Comput. 81 (1989) 249-264. | MR 1000065 | Zbl 0671.03023

[11] G. Winskel, A note on model checking the modal nu-calculus. Theoret. Comput. Sci. 83 (1991) 157-167. | Zbl 0745.68083