Model checking of non-finite state processes by finite approximations

  • N. De Francesco
  • A. Fantechi
  • S. Gnesi
  • P. Inverardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)


In this paper we present a verification methodology, using an action-based logic, able to check properties for full CCS terms, allowing also verification on infinite state systems. Obviously, for some properties we are only able to give a semidecision procedure. The idea is to use (a sequence of) finite state transition systems which approximate the, possibly infinite state, transition system corresponding to a term. To this end we define a particular notion of approximation, which is stronger than simulation, suitable to define and prove liveness and safety properties of the process terms.


Model Check Transition System Operational Semantic Finite Property Safety Property 
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.


  1. [1]
    J. C. M. Baeten, J. A. Bergstra, J. W. Klop. Deddability of bisimulation equivalence for processes generating context-free languages. Journal of ACM 40, 3, 1993, pp. 653–682.Google Scholar
  2. [2]
    G. Bruns. A practical technique for process abstraction. CONCUR'93, LNCS 715, pp. 37–49.Google Scholar
  3. [3]
    A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS, n. 54, October 1994, pp. 207–223.Google Scholar
  4. [4]
    O. Burkart, B. Steffen. Pushdown processes: Parallel Composition and Model Checking. Proceedings, CONCUR 94, LNCS 836, 1994, pp. 98–113.Google Scholar
  5. [5]
    E.M. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Toplas, 8 (2), 1986, pp. 244–263.Google Scholar
  6. [6]
    E.M. Clarke, O. Grumberg, D.E. Long. Model Checking and Abstraction. ACM Toplas, 16 (5), 1994, pp. 1512–1542.Google Scholar
  7. [7]
    R. Cleaveland, J. Parrow, B. Steffen. The Concurrency Workbench. Proceedings of Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science 407, Springer-Verlag, 1990, pp. 24–37.Google Scholar
  8. [8]
    D.Dams, O.Grumberg, R.Gerth. Automatic Verification of Abstract Interpretation of Reactive Systems: Abstractions Preserving ∀CTL*, ∃CTL*, CTL*. IFIP working conference on Programming Concepts, Methods and Calculi (PROCOMET'94), 1994.Google Scholar
  9. [9]
    N. De Francesco, P. Inverardi. Proving Finiteness of CCS Processes by Non-standard Semantics. Acta Informatica, 31 (1), 1994, pp. 55–80.Google Scholar
  10. [10]
    R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Network and ISDN systems, Vol. 25, No. 7, 1993, pp 761–778.Google Scholar
  11. [11]
    R. De Nicola, F. W. Vaandrager. Action versus State based Logics for Transition Systems. Proceedings Ecole de Printemps on Semantics of Concurrency. LNCS 469, 1990, pp. 407–419.Google Scholar
  12. [12]
    J.C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, J. Sifakis. A Toolbox for the Verification of LOTOS Programs. 14th ICSE, Melbourne, 1992, pp. 246–261.Google Scholar
  13. [13]
    J.C. Fernandez, L. Mounier. Verifying Bisimulations “On the Fly”. Formal Description Techniques, III, Elsevier Science Publisher, pp. 95–110, 1991.Google Scholar
  14. [14]
    J. C. Godskesen, K. G. Larsen, M. Zeeberg. TAV Users Manual. Internal Report, Aalborg University Center, Denmark, 1989.Google Scholar
  15. [15]
    M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM, 32, 1985, pp. 137–161.Google Scholar
  16. [16]
    H. Hungar, B. Steffen. Local Model Checking for Context-Free Processes. Proceedings, ICALP 93, LNCS 700, 1993, pp. 593–605Google Scholar
  17. [17]
    H. Hungar. Local Model Checking for Parallel Composition of Context-Free Processes. Proceedings, CONCUR 94, LNCS 836, 1994, pp. 114–128.Google Scholar
  18. [18]
    H. Huttel, C Stirling. Actions speak louder than words: Proving Bisimilarity for Context Free Processes. LICS 91, IEEE Computer Society Press, 1991, pp. 376–386.Google Scholar
  19. [19]
    E. Kindler. Safety and Liveness Properties: A Survey. Bulletin of the EATCS, 53, 1994, pp. 268–272.Google Scholar
  20. [20]
    E. Madelaine. Verification Tools from the Concur Project. Bulletin of EATCS 47, 1992, pp. 110–120.Google Scholar
  21. [21]
    E. Madelaine, D. Vergamini. AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. FORTE '89, North-Holland, 1990, pp. 61–66.Google Scholar
  22. [22]
    Z. Manna, A. Pnueli. The Anchored Version of the Temporal Framework, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Lecture Notes in Computer Science 354, Springer-Verlag, 1989, pp. 201–284.Google Scholar
  23. [23]
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  24. [24]
    D. Taubner. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. LNCS 369, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • N. De Francesco
    • 1
  • A. Fantechi
    • 1
    • 2
  • S. Gnesi
    • 2
  • P. Inverardi
    • 3
  1. 1.Dipartimento di Ingegneria dell'InformazioneUniv. di PisaItaly
  2. 2.Istituto di Elaborazione dell'InformazioneC.N.R.PisaItaly
  3. 3.Dip. di Matematica ApplicataUniv. dell'AquilaItaly

Personalised recommendations