Abstract
Symbolic approaches attack the state explosion problem by introducing implicit representations that allow the simultaneous manipulation of large sets of states. The most commonly used representation in this context is the Binary Decision Diagram (BDD). This paper takes the point of view that other structures than BDD's can be useful for representing sets of values, and that combining implicit and explicit representations can be fruitful. It introduces a representation of complex periodic sets of integer values, shows how this representation can be manipulated, and describes its application to the state-space exploration of protocols. Preliminary experimental results indicate that the method can dramatically reduce the resources required for state-space exploration.
This work was supported by the Esprit BRA action REACT and by the Belgian Incentive Program “Information Technology” — Computer Science of the future, initiated by the Belgian State — Prime Minister's Office — Science Policy Office. The scientific responsibility is assumed by its authors.
“Aspirant” (Research Assistant) for the National Fund for Scientific Research (Belgium).
Chapter PDF
Similar content being viewed by others
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
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, May 1993.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 428–439, Philadelphia, June 1990.
Randal E. Bryant. Symbolic boolean manipulation with ordered binarydecision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. 5th ACM Symposium on Principles of Programming Langages, 1978.
O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagram. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 23–32, Rutgers, June 1990. Springer-Verlag.
C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
J.C. Fernandez and L. Mounier. On the fly verification of behavioural equivalences and preorders. In Proc. 3rd Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 181–191, Aalborg, July 1991.
S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In Computer Aided Verification, Proc. 5th Int. Workshop, volume 697, pages 71–84, Elounda, Crete, June 1993. Lacture Notes in Computer Science, Springer-Verlag.
P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 176–185, Rutgers, June 1990. Springer-Verlag.
H. Greenberg. Integer Programming. Academic Press, New York, 1971.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149–164, April 1993.
N. Halbwachs. Delay analysis in synchronous programs. In Proc. 5th Workshop on Computer Aided Verification, volume 697, Elounda, Crete, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
G. J. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992. North-Holland.
G. J. Holzmann. Tracing protocols. AT&T Technical Journal, 64(12):2413–2434, 1985.
G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.
C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 189–196, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.
A.S. Krishnakumar. Reachability and recurrence in extended finite state machines: Modular vector addition systems. In Proc. 5th Workshop on Computer Aided Verification, volume 697, pages 110–122, Elounda, Crete, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
F. Kabanza, J.-M. Stévenne, and P. Wolper. Handling infinite temporal data. In Proc. of the 9th ACM Symposium on Principles of Database Systems, pages 392–403, Nashville Tennessee, 1990.
H. LeVerge. A note on Chernikova's algorithm. Research Report 1662, INRIA, Rennes, April 1992.
B. Lubachevsky. An approach to automating the verification of compact parallel coordination programs. I. Acta Informatica, 21:125–169, 1984.
K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
N. Mercouroff. Analyse sémantique de communications entre processus de programmes parallèles. Rapport de Recherche LIX/RR/90/09, Ecole Polytechnique, Palaiseau, France, September 1990.
K. Murty. Linear and Combinatorial Programming. Wiley, New York, 1976.
D. Peled. All from one, one for all: on model checking using representatives. In Proc. 5th Conference on Computer Aided Verification, Elounda, June 1993. Lecture Notes in Computer Science, Springer-Verlag.
A. Valmari. State space generation with induction. In Proc. Scandinavian Conference on Artificial Intelligence — 89, pages 99–115, Tampere, Finland, June 1989.
A. Valmari. A stubborn attack on state explosion. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 156–165, Rutgers, June 1990. Springer-Verlag.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
C.H. West. Generalized technique for communication protocol validation. IBM J. of Res. and Devel., 22:393–404, 1978.
P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proc. CONCUR '93, volume 715 of Lecture Notes in Computer Science, pages 233–246, Hildesheim, August 1993. Springer-Verlag.
M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In Proc. 5th Workshop on Computer Aided Verification, volume 697 pages 210–224, Elounda, Crete June 1993. Lecture Notes in Computer Science, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boigelot, B., Wolper, P. (1994). Symbolic verification with periodic sets. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_43
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_43
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive