Abstract
A Symbolic Reachability Graph (SRG) is a highly condensed representation of system state space built automatically from a specification of system in terms of Wellformed net. The building of such graph profits from the presence of object symmetries to aggregate either states or actions within symbolic representatives. In this paper, we show how to make operational the CTL* formal checking system presented in [1]. Our technique consists in exploiting the SRG by taking into account the object symmetries only if they leave the formula invariant. The difficulty to bypass is that SRG does not preserve explicitly the behavior of the objects specified within formulas. This leads to a new specification of system, from which we can prove that model checking through a state space is equivalent to model checking through the symbolic reachability graph.
Chapter PDF
Keywords
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.
References
E. Allen Emerson, A. Prasad Sistla, “Symmetry and Model Checking”, 5th conference on Computer Aided Verification (CAV), June 1993.
G. Chiola, C. Dutheillet, G. Franceschinis, S. Haddad, “On Well-formed Colored Nets and their Symbolic Reachability Graph”, proc. of 11th International Conference on Application and Theory of Petri Nets, Paris-France, June 1990.
G. Chiola, R. Gaeta, “Efficient Simulation of Parallel Architectures Exploiting Symmetric Well-formed Petri Net Models”, 6th International Workshop on Petri nets and Performance Models, Durham, NC, USA, October 1995.
E.M. Clarke, T. Filkorne, S. Jha, “Exploiting Symmetry In Temporal Logic Model Checking”, 5th Computer Aided Verification (CAV), June 1993.
E. Clarke,O. Grumberg,D. Long, “Verification Tools for Finite-State Concurrent Systems”, “A Decade of Concurrency — Reflections and Perspectives”, LNCS vol 803, 1994.
S. Haddad, JM. Ilié, B. Zouari, M. Taghelit, “Symbolic Reachability Graph and Partial Symmetries”, In Proc. of the 16th International Conference on Application and Theory of Petri Nets, pp 238–257, Torino, Italy, June 1995.
Z. Manna, A. Pnueli. “The temporal Logic of Reactive and Concurrent Systems: Specification”, Springer-Verlag, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ilié, J.M., Ajami, K. (1997). Model checking through symbolic reachability graph. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030598
Download citation
DOI: https://doi.org/10.1007/BFb0030598
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive