Advertisement

The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic

  • Roope Kaivola
  • Antti Valmari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)

Abstract

Temporal logic model checking is a useful method for verifying properties of finite-state concurrent systems. However, due to the state explosion problem modular methods like compositional minimisation based on semantic congruences are essential in making the verification task manageable. In this paper we show that the so-called CFFD-equivalence defined by initial stability, infinite traces, divergence traces and stable failures is exactly the weakest compositional equivalence preserving nexttimeless linear temporal logic with an extra operator distinguishing deadlocks from divergences. Furthermore, a slight modification of CFFD, called the NDFD-equivalence, is exactly the weakest compositional equivalence preserving standard nexttimeless linear temporal logic.

Keywords

Temporal Logic Reduction Algorithm Linear Temporal Logic 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [BB89]
    Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LOTOS, in The Formal Description Technique LOTOS, North-Holland, 1989, pp. 23–73Google Scholar
  2. [BC89]
    Bolognesi, T. & Caneve, M.: Equivalence Verification: Theory, Algorithms and a Tool, in The Formal Description Technique LOTOS, North-Holland, 1989, pp. 303–326Google Scholar
  3. [BCG87]
    Browne, M. C. & Clarke, E. M. & Grümberg, O.: Characterizing Kripke Structures in Temporal Logic, in Ehrig, H. & Kowalski, R. & Levi, G. & Montanari, U. (eds.): TAPSOFT '87, vol. I, LNCS, vol. 249, Springer-Verlag, 1987, pp. 256–270Google Scholar
  4. [CLM89]
    Clarke, E. M. & Long, D. & McMillan, K. L.: Compositional Model Checking, in Proceedings of the Fourth IEEE Symposium on Logic in Computer Science, 1989, pp. 353–362Google Scholar
  5. [CH90]
    Cleaveland, R. & Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence, in Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, LNCS, vol. 407, Springer-Verlag, 1990, pp. 11–23Google Scholar
  6. [CPS90]
    Cleaveland, R. & Parrow, J. & Steffen, B.: The Concurrency Workbench, in Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, LNCS, vol. 407, Springer-Verlag, 1990, pp. 24–37Google Scholar
  7. [EC80]
    Emerson, E. A. & Clarke, E. M.: Characterising Correctness Properties of Parallel Programs Using Fixpoints, in Proceedings of the 7th ICALP, LNCS, vol. 85, Springer-Verlag, 1980, pp. 169–181Google Scholar
  8. [GS90]
    Graf, S. & Steffen, B.: Compositional Minimization of Finite-State Processes, in Kurshan, R. P. & Clarke, E. M. (eds.): Proceedings of CAV'90, LNCS, vol. 531, Springer-Verlag, 1990, pp. 186–196Google Scholar
  9. [KV91]
    Kaivola, R. & Valmari, A.: Using Truth-Preserving Reductions to Improve the Clarity of Kripke-Models, in Baeten, J. C. M. & Groote, J. F. (eds.): Proceedings of CONCUR'91, LNCS, vol. 527, Springer-Verlag, 1991, pp. 361–375Google Scholar
  10. [KLVC92]
    Kemppainen, J. & Levanto, M. & Valmari, A. & Clegg, M.: ”ARA” Puts Advanced Reachability Analysis Techniques Together, in Proceedings of the Fifth Nordic Workshop in Programming Environment Research, Tampere University of Technology, Software Systems Laboratory Report 14, 1992Google Scholar
  11. [Lam83]
    Lamport, L.: What Good is Temporal Logic?, in Proceedings of the IFIP 9th World Computer Congress, 1983, pp. 657–668Google Scholar
  12. [LP85]
    Lichtenstein, O. & Pnueli, A.: Checking that Finite State Concurrent Programs Satisfy Their Linear Specification, in Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985, pp. 97–107Google Scholar
  13. [Mil89]
    Milner, R.: Communication and Concurrency, Prentice Hall, 1989Google Scholar
  14. [OH86]
    Olderog, E.-R. & Hoare, C. A. R.: Specification-Oriented Semantics for Communicating Processes, in Acta Informatica, vol. 23, 1986, pp. 9–66zbMATHMathSciNetCrossRefGoogle Scholar
  15. [Sti87]
    Stirling, C.: Comparing Linear and Branching Time Temporal Logics, University of Edinburgh, LFCS Report Series ECS-LFCS-87-24, 1987Google Scholar
  16. [Val90]
    Valmari, A.: Compositional State Space Generation, in Proceedings of the 11th International Conference on Application and Theory of Petri Nets, 1990, pp. 43–62, to appear also in Advances in Petri Nets 92, LNCS, Springer-Verlag, 1992Google Scholar
  17. [VT91]
    Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm, in Protocol Specification, Testing and Verification XI, North-Holland, 1991, pp. 3–18Google Scholar
  18. [VT92]
    Valmari, A. & Tienari, M.: Compositional Failure-based Semantic Models for Basic LOTOS, A manuscript submitted for publication, 1992, 30 p.Google Scholar
  19. [Wal87]
    Walker, D.: Bisimulation Equivalence and Divergence in CCS, University of Edinburgh, LFCS Report Series ECS-LFCS-87-29, 1987Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Roope Kaivola
    • 1
  • Antti Valmari
    • 2
  1. 1.Department of Computer ScienceUniversity of HelsinkiHelsinkiFinland
  2. 2.Computer Technology LaboratoryTechnical Research Centre of FinlandOuluFinland

Personalised recommendations