Article

Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems

Author:

Radu MateescuAuthors Info & Claims

TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Pages 281 - 295

Published: 08 April 2002 Publication History

Abstract

Model-checking is a popular technique for verifying finitestate concurrent systems, whose behaviour can be modeled using Labeled Transition Systems (Ltss). In this paper, we study the model-checking problem for the modal -calculus on acyclic LTSS. This has various applications of practical interest such as trace analysis, log information auditing, run-time monitoring, etc. We show that on acyclic LTSS, the full -calculus has the same expressive power as its alternation-free fragment. We also present two new local model-checking algorithms based upon a translation to boolean equation systems. The first algorithm handles -calculus formulas with alternation depth ad( ) 2 and has time complexity O (| | ² (| S |+| T |)) and space complexity O (| | ² | S |), where | S | and | T | are the number of states and transitions of the acyclic LTS and | | is the number of operators in . The second algorithm handles formulas with alternation depth ad( ) = 1 and has time complexity O (| | (| S | + | T |)) and space complexity O(| | | S |).

References

[1]

H. R. Andersen. Model checking and boolean graphs. Th. Co. Sci. , 126:3-30, 1994.

[2]

J. C. Bradfield and C. Stirling. Modal Logics and Mu-Calculi: an Introduction. In Handbook of Process Algebra , pp. 293-330, Elsevier, 2001.

[3]

E. Clarke, O. Grumberg, and D. Peled. Model Checking . MIT Press, 2000.

[4]

R. Cleaveland, M. Klein, and B. Steffen. Faster Model Checking for the Modal Mu-Calculus. In CAV'92 , LNCS vol. 663, pp. 410-422.

[5]

R. Cleaveland and B. Steffen. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. FM in Syst. Design , 2:121-147, 1993.

[6]

F. Dietrich, X. Logean, S. Koppenhoefer, and J-P. Hubaux. Testing Temporal Logic Properties in Distributed Systems. In IWTCS'98 , pp. 247-262, Kluwer, 1998.

[7]

X. Du, S. A. Smolka, and R. Cleaveland. Local Model Checking and Protocol Analysis. Springer STTT Journal , 2(3):219-241, 1999.

[8]

M. Ducassé. OPIUM: An Extendable Trace Analyzer for Prolog. Journal of Logic Programming , 39(1-3):177-224, 1999.

[9]

E. A. Emerson and C-L. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In LICS'86 , pp. 267-278, IEEE, 1986.

[10]

J-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP (CÆSAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In CAV'96 , LNCS vol. 1102, pp. 437-440.

[11]

M. J. Fischer and R. E. Ladner. Propositional Dynamic Logic of Regular Programs. Journal of Computer and System Sciences , (18):194-211, 1979.

[12]

H. Garavel. OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing. In TACAS'98 , LNCS vol. 1384, pp. 68-84. Full version available as INRIA Research Report RR-3352.

[13]

K. Ilgun, R. A. Kemmerer, and P. A. Porras. State Transition Analysis: A Rule-Based Intrusion Detection Approach. IEEE Tr. on Soft. Eng. , 21(3):181-199, 1995.

[14]

A. Ingolfsdottir and B. Steffen. Characteristic Formulae for Processes with Divergence. Information and Computation , 110(1):149-163, June 1994.

[15]

D. Kozen. Results on the Propositional µ-calculus. Th. Co. Sci. , 27:333-354, 1983.

[16]

K. G. Larsen. Efficient Local Correctness Checking. In CAV'92 , LNCS vol. 663, pp. 30-43.

[17]

X. Liu, C. R. Ramakrishnan, and S. A. Smolka. Fully Local and Efficient Evaluation of Alternating Fixed Points. In TACAS'98 , LNCS vol. 1384, pp. 5-19.

[18]

A. Mader. Verification of Modal Properties Using Boolean Equation Systems . VERSAL 8, Bertz Verlag, Berlin, 1997.

[19]

Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems , volume I (Specification). Springer Verlag, 1992.

[20]

R. Mateescu and M. Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. To appear in Science of Comp. Programming , 2002.

[21]

P. Stevens and C. Stirling. Practical Model-Checking Using Games. In TACAS'98 , LNCS vol. 1384, pp. 85-101.

[22]

C. Stirling. Modal and Temporal Properties of Processes . Springer Verlag, 2001.

[23]

I. Walukiewicz. A Complete Deductive System for the µ-calculus. In LICS'93 , pp. 136-147. Full version available as Brics Research Report RS-95-6, 1995.

[24]

B. Vergauwen and J. Lewi. Efficient Local Correctness Checking for Single and Alternating Boolean Equation Systems. In ICALP'94 , LNCS vol. 820, pp. 304-315.

Cited By

Genevès PLayaïda NSchmitt AGesbert N(2015)Efficiently Deciding μ-Calculus with Converse over Finite TreesACM Transactions on Computational Logic10.1145/272471216:2(1-41)Online publication date: 2-Apr-2015
https://dl.acm.org/doi/10.1145/2724712
Gutierrez JKlaedtke FLange M(2014)The µ-calculus alternation hierarchy collapses over structures with restricted connectivityTheoretical Computer Science10.1016/j.tcs.2014.03.027560:P3(292-306)Online publication date: 4-Dec-2014
https://dl.acm.org/doi/10.1016/j.tcs.2014.03.027
Friedmann OLange M(2011)The modal µ-calculus caught off guardProceedings of the 20th international conference on Automated reasoning with analytic tableaux and related methods10.5555/2029664.2029677(149-163)Online publication date: 4-Jul-2011
https://dl.acm.org/doi/10.5555/2029664.2029677
Show More Cited By

Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
1. Theory of computation
  1. Logic

Recommendations

Model Checking µ-Calculus in Well-Structured Transition Systems
TIME '04: Proceedings of the 11th International Symposium on Temporal Representation and Reasoning

We study the model checking problem for fixpoint logics in well-structured multiaction transition systems. P.A. Abdulla et al. (1996) and Finkel & Schnoebelen (2001) examined the decidability problem for liveness (reachability) and progress (eventuality)...
Model Checking Synchronized Products of Infinite Transition Systems
LICS '04: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science

has to deal with two aspects. The systems models are structured, often as products of components, and the specification logic has to be expressive enough to allow the formalization of reachability properties. The present paper is a study on what can be ...
Model Checking Modal Transition Systems Using Kripke Structures
VMCAI '02: Revised Papers from the Third International Workshop on Verification, Model Checking, and Abstract Interpretation

We reduce the modal mu-calculus model-checking problem for Kripke modal transition systems to the modal mu-calculus modelchecking problem for Kripke structures. This reduction is sound, preserves the alternation-depth fragments of the modal mu-calculus, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

April 2002

480 pages

ISBN:3540434194

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 April 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Genevès PLayaïda NSchmitt AGesbert N(2015)Efficiently Deciding μ-Calculus with Converse over Finite TreesACM Transactions on Computational Logic10.1145/272471216:2(1-41)Online publication date: 2-Apr-2015
https://dl.acm.org/doi/10.1145/2724712
Gutierrez JKlaedtke FLange M(2014)The µ-calculus alternation hierarchy collapses over structures with restricted connectivityTheoretical Computer Science10.1016/j.tcs.2014.03.027560:P3(292-306)Online publication date: 4-Dec-2014
https://dl.acm.org/doi/10.1016/j.tcs.2014.03.027
Friedmann OLange M(2011)The modal µ-calculus caught off guardProceedings of the 20th international conference on Automated reasoning with analytic tableaux and related methods10.5555/2029664.2029677(149-163)Online publication date: 4-Jul-2011
https://dl.acm.org/doi/10.5555/2029664.2029677
Mateescu ROudot E(2008)Improved On-the-Fly Equivalence Checking Using Boolean Equation SystemsProceedings of the 15th international workshop on Model Checking Software10.1007/978-3-540-85114-1_15(196-213)Online publication date: 10-Aug-2008
https://dl.acm.org/doi/10.1007/978-3-540-85114-1_15
Arenas MBarceló PLibkin L(2007)Combining temporal logics for querying XML documentsProceedings of the 11th international conference on Database Theory10.1007/11965893_25(359-373)Online publication date: 10-Jan-2007
https://dl.acm.org/doi/10.1007/11965893_25
Genevès PLayaïda NBulterman DBrailsford D(2006)Comparing XML path expressionsProceedings of the 2006 ACM symposium on Document engineering10.1145/1166160.1166182(65-74)Online publication date: 10-Oct-2006
https://dl.acm.org/doi/10.1145/1166160.1166182
Mateescu R(2003)A generic on-the-fly solver for alternation-free boolean equation systemsProceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems10.5555/1765871.1765881(81-96)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1765871.1765881

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents