Model checking for context-free processes

  • Olaf Burkart
  • Bernhard Steffen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


We develop a model-checking algorithm that decides for a given context-free process whether it satisfies a property written in the alternation-free modal mu-calculus. The central idea behind this algorithm is to raise the standard iterative model-checking techniques to higher order. in contrast to the usual approaches, in which the set of formulas that are satisfied by a certain state are iteratively computed, our algorithm iteratively computes a property transformer for each state class of the finite process representation. These property transformers can then simply be applied to solve the model-checking problem. The complexity of our algorithm is linear in the size of the system's representation and exponential in the size of the property being investigated.


Model Check Property Transformer Equational System Atomic Proposition Label Transition System 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BBK87]
    J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. In PARLE '87, LNCS 259, pages 94–113. Springer, 1987.Google Scholar
  2. [Bra91]
    J.C. Bradfield. Verifying Temporal Properties of Systems with Applications to Petri Nets. PhD thesis, University of Edinburgh, 1991.Google Scholar
  3. [Bry86]
    R.E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.Google Scholar
  4. [BS91]
    J.C. Bradfield and C. Stirling. Local Model Checking for Infinite State Spaces. Technical Report ECS-LFCS-90-115, LFCS, June 1991.Google Scholar
  5. [Cau90]
    D. Caucal. Graphes Canoniques de Graphes Algébriques. RAIRO, 24(4):339–352, 1990.zbMATHMathSciNetGoogle Scholar
  6. [CDS]
    R. Cleaveland, M. Dreimüller, and B. Steffen. Faster Model Checking for the Modal Mu-Calculus. Accepted for CAV '92.Google Scholar
  7. [CES86]
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.zbMATHCrossRefGoogle Scholar
  8. [Cle90]
    R. Cleaveland. Tableau-Based Model Checking in the Propositional Mu-Calculus. Acta Informatica, 27:725–747, 1990.zbMATHMathSciNetCrossRefGoogle Scholar
  9. [CPS89]
    R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench. In Proceedings of the Workshop on Automatic Verification Methods for Finite-State Systems, LNCS 407, pages 24–37. Springer, 1989.Google Scholar
  10. [CS91]
    R. Cleaveland and B. Steffen. Computing Behavioural Relations, Logically. In ICALP '91, LNCS 510. Springer, 1991.Google Scholar
  11. [CS92]
    R. Cleaveland and B. Steffen. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. In CAV '91, LNCS 575, pages 48–58. Springer, 1992.Google Scholar
  12. [EL86]
    E.A. Emerson and C.-L. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In Proc. 1th Annual Symp. on Logic in Computer Science, pages 267–278. IEEE Computer Society Press, 1986.Google Scholar
  13. [Gro91]
    J.F. Groote. A Short Proof of the Decidability of Bisimulation for Normed bpa-Processes. Technical Report CS-R9151, CWI, December 1991.Google Scholar
  14. [HS91]
    H. Hüttel and C. Stirling. Actions Speak Louder than Words: Proving Bisimularity for Context-Free Processes. In Proc. 6th Annual Symp. on Logic in Computer Science, pages 376–386. IEEE Computer Society Press, 1991.Google Scholar
  15. [HT92]
    D.T. Huynh and L. Tian. Deciding Bisimilarity of Normed Context-Free Processes is in 2p. Technical Report UTDCS-1-92, University of Texas at Dallas, 1992.Google Scholar
  16. [Koz83]
    D. Kozen. Results on the Propositional μ-Calculus. Theoretical Computer Science, 27:333–354, 1983.zbMATHMathSciNetCrossRefGoogle Scholar
  17. [Lar88]
    K.G. Larsen. Proof Systems for Hennessy-Milner Logic with Recursion. In CAAP '88, LNCS 299, pages 215–230. Springer, 1988.Google Scholar
  18. [SW89]
    C. Stirling and D. Walker. Local Model Checking in the Modal Mu-Calculus. In TAPSOFT '89, LNCS 351, pages 369–383. Springer, 1989.Google Scholar
  19. [Tar55]
    A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 5:285–309, 1955.zbMATHMathSciNetGoogle Scholar
  20. [Win89]
    G. Winskel. A Note on Model Checking the Modal Mu-Calculus. In Automata, Languages and Programming, LNCS 372, pages 761–772. Springer, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Olaf Burkart
    • 1
  • Bernhard Steffen
    • 1
  1. 1.Lehrstuhl für Informatik IIRWTH AachenAachenGermany

Personalised recommendations