Abstract
This paper deals with verification methods based on equivalence relations between labeled transition systems. More precisely, we are concerned by two practical needs: how to efficiently minimize and compare labeled transition systems with respect to bisimulation or simulation-based equivalence relations.
First, we recall the principle of the classical algorithms for the existing equivalence relations, which are based on successive partition refinements of the state space of the labeled transition systems under consideration. However, in spite of their theoretical efficiency, the main drawback of these algorithms is that they require to generate and to store in memory the whole labeled transition systems to be compared or minimized. Therefore, the size of the systems which can be handled in practice remains limited. We propose here another approach, allowing to combine the generation and the verification phases, which is based on two algorithms respectively devoted to the comparison (“on the fly” comparison) and the minimization (minimal model generation) of labeled transition systems. Then, we present the results obtained when implementing some of these algorithms within the tool Aldébaran.
This work was partially supported by ESPRIT Basic Research Action “SPEC” and french project research C3
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Bouajjani, J.C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching time semantics. In 18th ICALP, july 1991.
A. Bouajjani, J. C. Fernandez, and N. Halbwachs. On the verification of safety properties. Tech. report, Spectre L 12, IMAG, Grenoble, march 1990.
A. Bouajjani, J.C. Fernandez, and N. Halbwachs. Minimal model generation. In Workshop on Computer-aided Verification, to appear in LNCS, Springer Verlag, june 1990.
S. D. Brookes, C.A.R Hoare, and A.W. Roscoe. Theory of communicating sequential processes. JACM, 31(3), 1984.
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic spec ifications. TOPLAS, 8(2), 1986.
R. Cleaveland. On automatically distinguishing inequivalent processes. In Workshop on Computer-Aided Verification, june 1990.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. In Workshop on Computer-Aided Verification, june 1990.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In Workshop on Computer-Aided Verification, june 1990.
R. de Simone and D. Vergamini. Aboard Auto. Rapport Technique 111, INRIA, Sophia Antipolis, 1989.
J. C. Fernandez. An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming, 13(2–3), May 1990.
J.-C. Fernandez and L. Mounier. “on the fly” verification of behavioural equivalences and preorders. In Workshop on Computer-aided Verification, To appear, july 1–4 1991.
R.J. van Glabbeek. The Linear Time-Branching Time Spectrum. Technical Report CS-R9029, Centre for Mathematics and Computer Science, 1990.
Hubert Garavel and Joseph Sifakis. Compilation and verification of lotos specifications. In L. Logrippo, R. L. Probert, and H. Ural, editors, Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa), IFIP, North-Holland, Amsterdam, June 1990.
Jan Friso Groote and Frits Vaandrager. An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. CS-R 9001, Centrum voor Wiskunde en Informatica, Amsterdam, January 1990.
R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). CS-R 8911, Centrum voor Wiskunde en Informatica, Amsterdam, 1989.
Claude Jard and Thierry Jeron. On-line model-checking for finite linear temporal logic specifications. In International Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, Springer Verlag, 1989.
Claude Jard and Thierry Jéron. Bounded-memory algorithms for verification on-the-fly. In K. G. Larsen, editor, Proceedings of the 3rd Workshop on Computer-Aided Verification (Aalborg, Denmark), July 1991. to appear.
P. Kanellakis and S. Smolka. Ccs expressions, finite state processes and three problems of equivalence. In Proceedings ACM Symp. on Principles of Distribued Computing, 1983.
R. Milner. A calculus of communication systems. In LNCS 92, Springer Verlag, 1980.
R. De Nicola, U. Montanari, and F.W. Vaandrager. Back and Forth Bisimulations. CS-R 9021, Centrum voor Wiskunde en Informatica, Amsterdam, 1990.
R. De Nicola and F. Vaandrager. Three logics for branching bisimulation. In Proc. of Fifth Symp. on Logic in Computer Science, Computer Society Press, 1990.
D. Park. Concurrency and automata on infinite sequences. In 5th GI-Conference on Theorical Computer Science, Springer Verlag, 1981. LNCS 104.
R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM J. Comput., No. 6, 16, 1987.
Juan Quemada, Santiago Pavón, and Angel Fernández. Transforming lotos specifications with lola: the parametrized expansion. In Kenneth J. Turner, editor, Proceedings of the 1st International Conference on Formal Description Techniques FORTE'88 (Stirling, Scotland), pages 45–54, North-Holland, Amsterdam, September 1988.
A. Rasse. Error diagnosis in finite communicating systems. In Workshop on Computer-aided Verification, To appear, july 1–4 1991.
J.L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Xesar: A Tool for Protocol Validation. User's Guide. LGI-Imag, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernandez, JC., Mounier, L. (1991). A tool set for deciding behavioral equivalences. 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_78
Download citation
DOI: https://doi.org/10.1007/3-540-54430-5_78
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