Skip to main content
SpringerLink
Log in

Reduced labelled transition systems save verification effort

  • Selected Presentations
  • Conference paper
  • First Online:
CONCUR '91 (CONCUR 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 527))

Included in the following conference series:

Abstract

A new method for reducing the amount of effort in the verification of Basic Lotos specifications is presented. The method is based on generating a reduced labelled transition system (RLTS) of the specification. The RLTS captures the semantics of the specification in the sense of the semantic theory of CSP but it is typically much smaller than the ordinary labelled transition system (LTS) of the specification. Thus it can replace the LTS in the verification of the equivalence (in CSP sense) of two specifications. The method is demonstrated with a bounded buffer example where an exponential saving of states is achieved.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14 (1987) 25–59. Also: The Formal Description Technique LOTOS, North-Holland 1989, pp. 23–73.

    Google Scholar 

  2. Bolognesi, T. & Smolka, S. A.: Fundamental Results for the Verification of Observational Equivalence: A Survey. Protocol Specification, Testing and Verification VII, North-Holland, 1987, pp. 165–179.

    Google Scholar 

  3. Clarke, E. M. & Grümberg, O.: Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms. Proceedings of the 6th ACM Symposium on Principles of Distributed Computing, 1987, pp. 294–303.

    Google Scholar 

  4. Clarke, E. M., Long, D. E. & McMillan, K. L.: Compositional Model Checking. Proceedings of the Fourth IEEE Symposium of Logic in Computer Science, Asilomar, California, 1989.

    Google Scholar 

  5. Cleaveland, R., Parrow, J. & Steffen, B.: The Concurrency Workbench. Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 24–37.

    Google Scholar 

  6. Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods. Proceedings of the Workshop on Computer-Aided Verification, DIMACS Technical Report 90–31, Vol. I, 1990.

    Google Scholar 

  7. Godefroid, P. & Wolper, P.: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. To appear in the Proceedings of the Third Workshop on Computer Aided Verification, Aalborg, Denmark, July 1991.

    Google Scholar 

  8. Graf, S. & Steffen, B.: Compositional Minimization of Finite State Processes. Proceedings of the Workshop on Computer-Aided Verification, DIMACS Technical Report 90-31, Vol. I, 1990.

    Google Scholar 

  9. Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.

    Google Scholar 

  10. Itoh, M. & Ichikawa, H.: Protocol Verification Algorithm Using Reduced Reachability Analysis. Transactions of the IECE of Japan E66 Nr 2 1983 pp. 88–93.

    Google Scholar 

  11. Janicki, R. & Koutny, M.: Net Implementation of Optimal Simulations. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, pp. 295–314.

    Google Scholar 

  12. Jensen, K.: Coloured Petri Nets. Petri Nets, Central Models and Their Properties, Lecture Notes in Computer Science 254, Springer-Verlag 1987, pp. 248–299.

    Google Scholar 

  13. Karp, R. M. & Miller, R. E.: Parallel Program Schemata. Journal of Computer and System Sciences 3 (1969) pp. 147–195.

    Google Scholar 

  14. Lindqvist, M.: Parameterized Reachability Trees for Predicate/Transition Nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, pp. 22–42.

    Google Scholar 

  15. Mazurkiewicz, A.: Trace Theory. Petri Nets, Applications and Relationships to Other Models of Concurrency, Lecture Notes in Computer Science 255, Springer-Verlag 1987, pp. 279–324.

    Google Scholar 

  16. Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.

    Google Scholar 

  17. Olderog, E.-R. & Hoare, C. A. R.: Specification-Oriented Semantics for Communicating Processes. Acta Informatica 23, 1986, pp. 9–66.

    Google Scholar 

  18. Overman, W. T.: Verification of Concurrent Systems: Function and Timing. PhD Thesis, University of California Los Angeles 1981, 174 p.

    Google Scholar 

  19. Pnueli, A.: Applications of Temporal Logic to the Specification and Verification of Concurrent Systems: A Survey of Current Trends. Current Trends in Concurrency, Lecture Notes in Computer Science 224, Springer-Verlag 1986, pp. 510–584.

    Google Scholar 

  20. Quemada, J., Pavón, S. & Fernández, A.: State Exploration by Transformation with LOLA. Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 294–302.

    Google Scholar 

  21. Valmari, A.: Error Detection by Reduced Reachability Graph Generation. Proceedings of the Ninth European Workshop on Application and Theory of Petri Nets, Venice, Italy 1988, pp. 95–112.

    Google Scholar 

  22. Valmari, A.: Heuristics for Lazy State Generation Speeds up Analysis of Concurrent Systems. Proceedings of the Finnish Artificial Intelligence Symposium STeP-88, Helsinki 1988, Vol. 2 pp. 640–650.

    Google Scholar 

  23. Valmari, A.: State Space Generation: Efficiency and Practicality. PhD Thesis, Tampere University of Technology Publications 55, 1988, 169 p.

    Google Scholar 

  24. Valmari, A.: Eliminating Redundant Interleavings during Concurrent Program Verification. Proceedings of Parallel Architectures and Languages Europe '89 Vol. 2, Lecture Notes in Computer Science 366, Springer-Verlag 1989 pp. 89–103.

    Google Scholar 

  25. Valmari, A.: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491–515. (An earlier version appeared in Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn 1989, Vol. 2 pp. 1–22.)

    Google Scholar 

  26. Valmari, A.: State Space Generation with Induction (Short Version). Scandinavian Conference on Artificial Intelligence-89, Frontiers in Artificial Intelligence and Applications, IOS, Amsterdam 1989, pp. 99–115.

    Google Scholar 

  27. Valmari, A.: A Stubborn Attack on State Explosion. Computer-Aided Verification '90, AMS DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol 3, pp. 25–41. Also in Proceedings of the Workshop on Computer-Aided Verification, DIMACS Technical Report 90-31, Vol. I, 1990.

    Google Scholar 

  28. Valmari, A.: Compositional State Space Generation. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris 1990, pp. 43–62.

    Google Scholar 

  29. Valmari, A.: Stubborn Sets of Coloured Petri Nets. To appear in the Proceedings of the 12th International Conference on Application and Theory of Petri Nets, Aarhus, Denmark 1991. 20 p.

    Google Scholar 

  30. Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. To appear in the proceedings of the 11th International IFIP WG 6.1 Symposium on Protocol Specification, Testing and Verification 1991, Stockholm, Sweden, June 1991. 16 p.

    Google Scholar 

  31. Vuong, S. T., Hui, D. D. & Cowan, D. D.: Valira — A Tool for Protocol Validation via Reachability Analysis. Protocol Specification, Testing and Verification VI, North-Holland 1987, pp. 35–41.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technical Research Centre of Finland Computer Technology Laboratory, PO Box 201, SF-90571, Oulu, Finland

    Antti Valmari & Matthew Clegg

Authors
  1. Antti Valmari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthew Clegg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jos C. M. Baeten Jan Frisco Groote

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Valmari, A., Clegg, M. (1991). Reduced labelled transition systems save verification effort. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_111

Download citation

  • DOI: https://doi.org/10.1007/3-540-54430-5_111

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54430-2

  • Online ISBN: 978-3-540-38357-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation