Abstract
The control state reachability problem is decidable for well-structured infinite-state systems like unbounded Petri Nets, Vector Addition Systems, Lossy Petri Nets, and Broadcast Protocols. An abstract algorithm that solves the problem is given in [AČJT96,FS99]. The algorithm computes the closure of the predecessor operator w.r.t. a given upward-closed set of target states. When applied to this class of verification problems, traditional (infinite-state) symbolic model checkers suffer from the state explosion problem even for very small examples. We provide BDD-like data structures to represent in a compact way collections of upwards closed sets over numerical domains. This way, we turn the abstract algorithm of [AČJT96,FS99] into a practical method. Preliminary experimental results indicate the potential usefulness of our method.
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
P. A. Abdulla, K. Čerāns, B. Jonsson, and Y.-K. Tsay. General Decidability Theorems for Infinite-state Systems. In Proceedings of the 11th Annual. Symposium on Logic in Computer Science (LICS’96), pages 313–321. IEEE Computer Society Press, 1996. 426, 427, 428, 436, 437, 438
P. A. Abdulla, B. Jonsson, M. Kindahl, and D. Peled. A General Approach to Partial Order Reductions in Symbolic Verification. In Proceedings of the 10th Conference on Computer Aided Verification (CAV’98), volume 1427 of LNCS, pages 379–390. Springer, 1998. 426, 438
BLP+99._G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In Proceedings of the 11th Conference on Computer Aided Verification (CAV’99), volume 1633 of LNCS, pages 341–353. Springer 1999. 438
B. Boigelot, P. Wolper. Verifying systems with infinite but regular state space. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV’98), volume 1427 of LNCS, pages 88–97. Springer, 1998. 426
A. Bouajjani and R. Mayr. Model Checking Lossy Vector Addition Systems. In Proceedings of the 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS’99), volume 1563 of LNCS, pages 323–333. Springer, 1999. 426
R. E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transaction on Computers, C-35(8):667–691, August, 1986. 437
T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinite-state Systems using Presburger Arithmetics. In Proc. 9th Conf. on Computer Aided Verification (CAV’97), LNCS 1254, pages 400–411. Springer-Verlag, 1997. 427, 437
BCB+90._J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pages 428–439. IEEE Computer Society Press, 1990. 426, 427
K. Čerāns. Deciding Properties of Integral Relational Automata. In Proceedings of the International Conferences on Automata and Languages for Programming (ICALP 94), volume 820 of LNCS, pages 35–46. Springer, 1994. 426
G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In Proceedings of the 15th Int. Conf. on Application and Theory of Petri Nets 1994, LNCS 815, pages 179–198. Springer-Verlag, 1994. 426
E. Clarke, M. Fujita, and X. Zhao. Multi-terminal Binary Decision Diagrams and Hybrid Decision Diagrams. In Representations of Discrete Functions, pages 93–108. Kluwer Academic Publishers, 1996. 437
G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL’99), volume 1683 of LNCS, pag. 50–66. Springer, 1999. 426, 427, 436, 437
G. Delzanno and A. Podelski, Model Checking in CLP. In W. R. Cleaveland, editor, Proc. 5th Int. Con. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99)., LNCS 1579, pages 223–239. Springer-Verlag, 1999.
G. Delzanno and J. F. Raskin. Symbolic Representation of Upward-Closed Sets. Technical report MPI-I-1999-2-007, Max-Planck-Institut für Informatik, November 1999. Available on the web at http://www.mpisb.mpg.de/units/ag2/. 428, 437
E. A. Emerson and K. S. Namjoshi. On Model Checking for Nondeterministic Infinite-state Systems. In Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS’ 98), pages 70–80. IEEE Computer Society Press, 1998. 426
J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS’99), pages 352–359. IEEE Computer Society Press, 1999. 426
A. Finkel. Reduction and Covering of Infinite Reachability Trees. Information and Computation 89(2), pages 144–179. Academic Press, 1990. 426
A. Finkel and P. Schnoebelen. Well-structured Transition Systems Everywhere! Theoretical Computer Science, 1999. To appear. 426, 427, 428
F. Gagnon, J.-Ch. Grégoire, and D. Zampuniéris. Sharing Trees for ‘On-the-fly’ Verification. In Proceedings of the International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE’95), 1995. 437
B. Grahlmann. The PEP Tool. In Proceedings of the 9th Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 440–443. Springer, 1997. 438
M. R. Henzinger, T. A. Henzinger, P. K. Kopke. Computing Simulations on Finite and Infinite Graphs. In Proceedings of the 36th Annual IEEE Symposium on Foundations of Computer Science (FOCS’95), pages 453–462. IEEE Society Press, 1995. 434
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a Model Checker for Hybrid Systems. In Proceedings of the 9th Conference on Computer Aided Verification (CAV’97), volume 1254 of LNCS, pages 460–463. Springer, 1997. 427
K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.
N. M. Minsky. Finite and Infinite Machines. Prentice Hall, Englewood Cliffs, N.Y., 1967. 426
SKM+90._A. Srinivasan, T. Kam, S. Malik, and R. K. Brayton. Algorithms for Discrete Functions Manipulation. In Proceedings of the IEEE International. Conference on Computer-Aided Design (ICCAD’90), 1990. 437
K. Strehl, L. Thiele. Interval Diagram Techniques For Symbolic Model Checking of Petri Nets. In Proceedings of the Design, Automation and Test in Europe Conference (DATE’99), pages 756–757, 1999. 438
E. Teruel. Structure Theory of Weighted Place/Transition Net Systems: The Equal Conflict Hiatus. Ph.D. Thesis, University of Zaragoza, 1994. 426, 427, 436
G. Wimmel. A BDD-based Model Checker for the PEP Tool. Technical Report, University of Newcastle Upon Tyne, 1997. 438
D. Zampuniéris. The Sharing Tree Data Structure: Theory and Applications in Formal Verification. PhD Thesis. Facultés Universitaires Notre-Dame de la Paix, Namur, Belgium, May 1997. 427, 436, 437
D. Zampuniéris, and B. Le Charlier. Efficient Handling of Large Sets of Tuples with Sharing Trees. In Proceedings of the Data Compressions Conference (DCC’95), 1995. 427, 429, 430, 431, 432, 435
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delzanno, G., Raskin, JF. (2000). Symbolic Representation of Upward-Closed Sets. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_29
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive