Abstract
In this paper we considered two different fragments of μ-calculus, logics L 1 and L 2. We gave model checking algorithms for logics L 1 and L 2 which are of complexity O(m 2 n) where m is the length of the formula and n is the size of the structure. We have shown that the logic L 2 is as expressive as ECTL* given in [13]. In additions to these results, we have shown that the model checking problem for the μ-calculus is equivalent to the non-emptiness problem of parity tree automata.
It will be interesting to investigate if there is a model checking algorithm for the logics L 1 and L 2 which is only of complexity O(mn) instead of O(m 2 n. Of course, determining if the model checking problem for the full μ-calculus is in P or not, is also an open problem.
This author's research is supported in part by the ONR grant N00014-89-J-1472 and Texas Advanced Technology Program Grant 003658-250.
This author's research is supported in part by NSF grant CCR-9212183.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Cleaveland, Tableux-based model checking in the propositional μ-calculus, Acta Informatica, 27:725–747, 1990.
R. Cleaveland and B. Steffen, A linear-time model-checking for alternation free modal fi-calculus, Proceedings of the 3rd workshop on Computer Aided Verification, Aalborg, LNCS, Springer-Verlag, July 1991.
R. Cleaveland and B. Steffen, Faster model-checking for modal μ-calculus, Proceedings of the 4th workshop on Computer Aided Verification, Montreal, July 1991.
E. A. Emerson, E. M. Clarke, Characterizing correctness properties of parallel programs Using Fixpoints, Proceedings of the International Conference on Automata, Languages and Programming, 1980.
E.A. Emerson and C. S. Jutla, Tree Automata, Mu-calculus and Determinacy, Proceedings of the 1991 IEEE Symposium on Foundations of Computer Science.
E. A, Emerson and C. Leis, Efficient model-checking in fragments of μ-calculus, Proceedings of Symposium on Logic in Computer Science, 1986.
E. A. Emerson and C. Leis, Modalities for Model Checking, Science of Computer Programming, 1987.
D. Kozen, Results on the propositional μ-calculus, Theoretical Computer Science, 27, 1983.
A.W. Mostowski, Regular Expressions for Infinite trees and a standard form of automata, in: A. Skowron, ed., Computation Theory, LNCS, vol 208, 1984, Springer-Verlag.
D. Niwinski, Fixed-points Vs. Infinite Generation, Proceedings of the Third IEEE Symposium on Logic in Computer Science, 1988.
C. Stirling, D. Walker, Local model-checking in modal μ-calculus, Proceedings of TAPSOFT, 1989.
R. S. Streett and E. A. Emerson, An automata theoretic decision procedure for Propositional μ-calculus, Proceedings of the International Conference on Automata, Languages and Programming, 1984.
M. Vardi and P. Wolper, Yet Another Process Logic, Proceedings of the workshop on Logics of Programs, Pittsburgh, 1983, also appeared in Lecture Notes in Computer Science.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Jutla, C.S., Sistla, A.P. (1993). On model-checking for fragments of μ-calculus. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_32
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive