Skip to main content
SpringerLink
Log in

A linear-time model-checking algorithm for the alternation-free modal mu-calculus

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We develop a model-checking algorithm for a logic that permits propositions to be defined using greatest and least fixed points of mutually recursive systems of equations. This logic is as expressive as the alternation-free fragment of the modal mu-calculus identified by Emerson and Lei, and it may therefore be used to encode a number of temporal logics and behavioral preorders. Our algorithm determines whether a process satisfies a formula in time proportional to the product of the sizes of the process and the formula; this improves on the best known algorithm for similar fixed-point logics.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications.ACM TOPLAS, 8(2):244–263 (1986).

    Google Scholar 

  2. J.-C. Fernandez.Aldébaran: Une Système de Vérification par Réduction de Processus Communicants. Ph.D. Thesis, Université de Grenoble, (1988).

  3. J. Malhotra, S.A. Smolka, A. Giacalone, and R. Shapiro. Winston: A tool for hierarchical design and simulation of concurrent systems.Proceedings of the Workshop on Specification and Verification of Concurrent Systems, University of Stirling, Scotland, pp. 140–152 (1988).

  4. J. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in Xesar of the sliding window protocol. InProceedings 7th Symp. on Protocol Specification, Testing, and Verification, Zurich, pp. 235–250 (1987).

  5. V. Roy and R. de Simone. Auto/Autograph. InComputer-Aided Verification '90, Piscataway, NJ, pp. 477–491 (1990).

  6. R. Cleaveland and B. Steffen. When is ‘partial’ complete? A logic-based proof technique using partial specifications.Proceedings of the Fifth Symposium on Logic in Computer Science, Philadelphia, PA, pp. 440–449 (1990).

  7. S. Graf and B. Steffen. Using interface specifications for compositional reduction.Computer-Aided Verification '90, pp. 57–76 (1990).

  8. R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench.Proceedings Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science, 407:24–37 (1989). Also to appear inACM TOPLAS.

  9. R. Cleaveland, J. Parrow, and B. Steffen. A semantics-based verification tool for finite-state systems.Proceedings of the 9th Symposium on Protocol Specification, Testing, and Verification, Enschede, Holland, pp. 287–302 (1989).

  10. R. Cleaveland and B. Steffen. “Computing Behavioural Relations, Logically.” InProceedings of the Eighteenth International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 510:127–138 (1991).

  11. B.U. Steffen and A. Ingólfsdóttir. Characteristic formulae for CCS with divergence. To appear inInformation and Computation.

  12. E.A. Emerson, and C.-L. Lei, Efficient model checking in fragments of the propositional mucalculus.Proceedings of the First Symposium on Logic in Computer Science, Cambridge, MA, pp. 267–278 (1986).

  13. M. Fischer and R. Ladner. Propositional dynamic logic of regular programs.Journal of Computer and System Sciences, 18:194–211 (1979).

    Google Scholar 

  14. D. Kozen. Results on the propositional μ-calculus.Theoretical Computer Science, 27:333–354 (1983).

    Google Scholar 

  15. K. Larsen. Proof systems for Hennessy-Milner logic with recursion.Proceedings of Colloque sur Algèbre et Arbres en Programmation, Nancy, France, pp. 215–230 (1988).

  16. A. Tarski. A lattice-theoretical fixpoint theorem and its applications.Pacific Journal of Mathematics 25(2):285–309 (1955).

    Google Scholar 

  17. A. Arnold and P. Crubille. A linear algorithm to solve fixed-point equations on transition systems.Information Processing Letters, 29:57–66 (September 1988).

    Google Scholar 

  18. D. Walker. Bisimulations and divergence.Proceedings of the Third Symposium on Logic in Computer Science, Edinburgh, Scotland, pp. 186–192 (1988).

  19. R. Cleaveland and M.C.B. Hennessy. Testing equivalence as a bisimulation equivalence.Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, Lecture Notes in Computer Science, 407:11–23 (1989). Also to appear inFundamental Aspects of Computing.

    Google Scholar 

  20. B.U. Steffen. Characteristic formulae. InProceedings of the Sixteenth International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 372:723–733 (1989).

  21. R. Cleaveland, M. Dreimüller, and B. Steffen. Faster model-checking for the modal mu-calculus. To appear inProceedings of the 1992 Workshop on Computer-Aided Verification. Lecture Notes in Computer Science.

  22. H. Andersen. Model checking and Boolean graphs.Proceedings of ESOP '92, Rennes, France, pp. 1–19, Springer-Verlag (1992).

  23. R. Cleaveland. Tableau-based model-checking in the propositional mu-calculus.Acta Information, 27:725–747 (1990).

    Google Scholar 

  24. C. Stirling and D. Walker. Local model checking in the modal mu-calculus. InProceedings of TAPSOFT '89, Lecture Notes in Computer Science, 351:369–383 (1989).

  25. G. Winskel. “Model checking in the modalv-calculus.” InProceedings of the Sixteenth International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 372:761–772 (1989).

  26. K. Larsen. Efficient local correctness checking. To appear inProceedings of the 1992 Workshop on Computer-Aided Verification.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, North Carolina State University, 27695-8206, Raleigh, NC, USA

    Rance Cleaveland

  2. Lehrstuhl für Informatik II, Rheinisch-Westfälische Technische Hochschule Aachen, D-5100, Aachen, Germany

    Bernhard Steffen

Authors
  1. Rance Cleaveland
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Cleaveland, R., Steffen, B. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form Method Syst Des 2, 121–147 (1993). https://doi.org/10.1007/BF01383878

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01383878

Keywords

Search

Navigation