Abstract
We describe the implementation, within Aldébaran of an algorithmic method allowing the generation of a minimal labeled transition system from an abstract model; this minimality is relative to an equivalence relation. The method relies on a symbolic representation of the state space. We compute the minimal labeled transition system using the Binary Decision Diagram structures to represent the set of equivalence classes. Some experiments are presented, using a model obtained from LOTOS specifications.
This work was partially supported by ESPRIT Basic Research Action “SPEC”
Chapter PDF
References
A. Arnold and M. Nivat. Comportement de processus. Les mathématiques de l'informatique, 1982.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic Model Checking: 1020 states and beyond. Technical Report, Carnegie Mellon University, 1989.
A. Bouali and R. de Simone. Symbolic bisimulation minimisation. In Fourth Workshop on Computer-Aided Verification,Montreal, June 1992.
A. Bouajjani, J.C. Fernandez, and N. Halbwachs. Minimal model generation. In Workshop on Computer-aided Verification, Rutgers, American Mathematical Society, Association for Computing Machinery, June 1990.
A. Bouajjani, J.C. Fernandez, N. Halbwachs, C. Ratel, and P. Raymond. Minimal state graph generation. Science of Computer Programming, 18(3), June 1992.
S. Bainbridge and L. Mounier. Specification and Verification of a Reliable Multicast Protocol. Software Engineering Department Technical Report HPL-91-63, Hewlett-Packard Laboratories, Bristol, U.K, 1990.
R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th POPL, january 1977.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In 5th. Annual Symp. on Principles of Programming Languages, pages 84–87, 1977.
R. Enders, T. Filkorn, and D. Taubner. Generating bdds for symbolic model checking in ccs. In Proceedings of the 3rd Workshop on Computer-Aided Verification (Aalborg, Denmark), 1991.
J. C. Fernandez. An implementation of an efficient algorithm foi bisimulation equivalence. Science of Computer Programming, 13(2–3), May 1990.
J.Cl. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A tool box for the verification of lotos programs. In 14th International Conference on software Engineering, 11–15 May 1992.
J.-C. Fernandez and L. Mounier. “on the fly” verification of behavioural equivalences and preorders. In Workshop on Computer-aided Verification, Aalborg University, Denmark, LNCS 575, Springer Verlag, July 1–4 1991.
J.Cl. Fernandez and L. Mounier. A tool set for deciding behavioural equivalences. In J.F. Groote J.C.M. Baeten, editor, CONCUR'91, Concurrency theory, LNCS 527, Springer Verlag, august 26–29 1991.
J.C. Godskesen, K. Larsen, and M. Zeeberg. Tav, tools for automatic verification. In Proceedings of the 1st International Workshop on Automatic Verification Methods for Finite State Systems (Grenoble, France), Springer Verlag, jun 1989.
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.
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.
ISO. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Draft International Standard 8807, International Organization for Standardization-Information Processing Systems — Open Systems Interconnection, Genève, July 1987.
P. Kanellakis and S. Smolka. Ccs expressions, finite state processes and three problems of equivalence. Information and Computation, 86(1), May 1990.
D. Lee and M. Yanakakis. Online minimization of transition systems. In ACM STOC 92, Vancouver, B.C., 1992.
R. Milner. A calculus of communication systems. In LNCS 92, Springer Verlag, 1980.
L. Mounier. Méthodes de Vérification de Spécifications Comportementales: étude et mise en oeuvre. PhD thesis, Université de Grenoble, 1992.
R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM J. Comput., No. 6, 16, 1987.
S. K. Shrivastava and P. D. Ezhilchelvan. rel/REL: A Family of Reliable Multicast Protocol for High-Speed Networks. Technical Report, University of Newcastle, Dept. of Computer Science, U.K, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernandez, J.C., Kerbrat, A., Mounier, L. (1993). Symbolic equivalence checking. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_8
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive