# Model checking of non-finite state processes by finite approximations

Conference paper

First Online:

- 4 Citations
- 239 Downloads

## Abstract

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.

## Keywords

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.

Download
to read the full conference paper text

## References

- [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]G. Bruns. A practical technique for process abstraction. CONCUR'93, LNCS 715, pp. 37–49.Google Scholar
- [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]O. Burkart, B. Steffen. Pushdown processes: Parallel Composition and Model Checking. Proceedings, CONCUR 94, LNCS 836, 1994, pp. 98–113.Google Scholar
- [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]E.M. Clarke, O. Grumberg, D.E. Long. Model Checking and Abstraction. ACM Toplas, 16 (5), 1994, pp. 1512–1542.Google Scholar
- [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]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]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]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]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]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]J.C. Fernandez, L. Mounier. Verifying Bisimulations “On the Fly”. Formal Description Techniques, III, Elsevier Science Publisher, pp. 95–110, 1991.Google Scholar
- [14]J. C. Godskesen, K. G. Larsen, M. Zeeberg. TAV Users Manual. Internal Report, Aalborg University Center, Denmark, 1989.Google Scholar
- [15]M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency.
*Journal of ACM*,**32**, 1985, pp. 137–161.Google Scholar - [16]H. Hungar, B. Steffen. Local Model Checking for Context-Free Processes. Proceedings, ICALP 93, LNCS 700, 1993, pp. 593–605Google Scholar
- [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]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]E. Kindler. Safety and Liveness Properties: A Survey. Bulletin of the EATCS, 53, 1994, pp. 268–272.Google Scholar
- [20]E. Madelaine. Verification Tools from the Concur Project. Bulletin of EATCS 47, 1992, pp. 110–120.Google Scholar
- [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]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]R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
- [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