Abstract
It has been known at least since 1983 that the checking of failure equivalence of two labelled transition systems is a PSPACE-complete problem, while the same problem for observation equivalence can be solved in roughly cubic time. Correspondingly, a widespread belief has arisen that failure-based equivalences are slower for the verification of concurrent systems than observation equivalence. In this article it is shown that this belief is based on a misinterpretation of the theoretical complexity result. Both theoretical and experimental evidence is given to the claim that failure-based equivalences are often faster in practice than observation equivalence. It is argued that the weakest congruence preserving given properties is in a certain sense optimal for the verification of those properties. Results giving weakest congruences for several verification tasks are surveyed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Kanellakis, P. C. & Smolka, S. A.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Proceedings of the 2nd Annual ACM Symposium on Principles of Distributed Computing, Montreal, Canada, August 1983, pp. 228–240.
Kanellakis, P. C. & Smolka, S. A.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation 86 (1990) pp. 43–68.
Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.
Brookes, S. D., Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating Sequential Processes. Journal of the ACM, 31 (3) 1984, pp. 560–599.
Brookes, S. D. & Rounds, W. C.: Behavioural Equivalence Relationships Induced by Programming Logics. Proceedings of 10th International Conference on Automata, Languages, and Programming, Barcelona, Spain, Lecture Notes in Computer Science 154, Springer-Verlag 1983, pp. 97–108.
Fernandez, J.-C.: An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming 13 (1989/90) 219–236.
Eloranta, J.: Minimizing the Number of Transitions with Respect to Observation Equivalence. BIT 31 (1991), 576–590.
Inverardi, P. & Priami, C.: Evaluation of Tools for the Analysis of Communicating Systems. EATCS Bulletin 45, October 1991, pp. 158–185.
Bouajjani, A., Fernandez, J.-C. & Halbwachs, N.: Minimal Model Generation. Computer-Aided Verification ’90 (Proceedings of a Workshop), AMS-ACM DIM ACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, American Mathematical Society 1991, pp. 85–91.
Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. Department of Computer Science, University of Helsinki, Report A- 1992-4, Helsinki, Finland 1992, 57 p.
Brinksma, E.: A Theory for the Derivation of Tests. Protocol Specification, Test-ing and Verification VIII (Proceedings of International IFIP WG 6.1 Symposium, 1988), North-Holland 1988, pp. 63–74.
Courcoubetis, C., Vardi, M., Wolper, P. & Yannakakis, M.: Memory Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in Sys-tem Design, 1: 275–288 (1992).
Valmari, A.: On-the-fly Verification with Stubborn Sets. Proceedings of CAV’93, 5th International Conference on Computer-Aided Verification, Elounda, Greece, Lecture Notes in Computer Science 697, Springer-Verlag 1993, pp. 397–408.
Madelaine, E. & Vergamini, D.: AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. Formal Description Techniques II (Proceedings of FORTE ’89), North-Holland 1990, pp. 61–66.
Graf, S. & Steffen, B.: Compositional Minimization of Finite State Processes. Computer-Aided Verification ’90 (Proceedings of a workshop), AMS-ACM DIM ACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, American Mathematical Society 1991, pp. 57–73.
Valmari, A.: Compositional State Space Generation. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 427–457.
Räuchle, T. & Toueg, S.: Exposure to Deadlock for Communicating Processes is Hard to Detect. Information Processing Letters 21 (1985) pp. 63–68.
Jones, N. D., Landweber, L. H. & Lien, Y. E.: Complexity of Some Problems in Petri Nets. Theoretical Computer Science 4 (1977) pp. 277–299.
Valmari, A.: Some Polynomial Space Complete Concurrency Problems. Tampere University of Technology, Software Systems Laboratory, Report 4, 1988, 34 p.
Hopcroft, J. E. & Ullman, J. D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley 1979, 418 p.
Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. Protocol Specification, Testing and Verification XI, North-Holland 1991, pp. 3–18.
Eloranta, J.: Minimal Transition Systems with Respect to Divergence Preserving Behavioural Equivalences. Doctoral thesis, University of Helsinki, Department of Computer Science, Report A-1994-1, Helsinki, Finland 1994, 162 p.
Rabinovich, A.: Checking Equivalences Between Concurrent Systems of Finite Agents (Extended Abstract). Proceedings of ICALP 92, Lecture Notes in Computer Science 623, Springer-Verlag 1992, pp. 696–707.
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.
Valmari, A., Kemppainen, J., Clegg, M. & Levanto, M.: Putting Advanced Reachability Analysis Techniques Together: the “ARA” Tool. Proceedings of Formal Methods Europe ’93, Lecture Notes in Computer Science 670, Springer-Verlag 1993, pp. 597–616.
Bolognesi, T. & Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14, 1987, pp. 25–59. Also in: The Formal Description Technique LOTOS, North-Holland 1989, pp. 23–73.
Valmari, A. & Tienari, M.: Compositional Failure-Based Semantic Models for Basic LOTOS. To appear in Formal Aspects of Computing, 29 p.
Valmari, A.: The Weakest Deadlock-Preserving Congruence. To appear in Infor-mation Processing Letters.
Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.
Bergstra, J. A., Klop, J. W. & Olderog, E.-R.: Failures without Chaos: A New Process Semantics for Fair Abstraction. Formal Description of Programming Concepts III, North-Holland, 1987, pp. 77–103.
Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Sys-tems: Specification. Springer-Verlag 1992, 427 p.
Kaivola, R. & Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. Proceedings of CONCUR ’92, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.
Setälä, M. & Valmari, A.: Validation and Verification with Weak Process Semantics. Proceedings of Nordic Seminar on Dependable Computing Systems 1994, Lyngby, Denmark, August 1994, pp. 15–26.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 British Computer Society
About this paper
Cite this paper
Valmari, A. (1995). Failure-based Equivalences Are Faster Than Many Believe. In: Desel, J. (eds) Structures in Concurrency Theory. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3078-9_22
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3078-9_22
Publisher Name: Springer, London
Print ISBN: 978-3-540-19982-3
Online ISBN: 978-1-4471-3078-9
eBook Packages: Springer Book Archive