Abstract
We propose a new symbolic model checking algorithm for parameterized concurrent systems modeled as (Lossy) Petri Nets, and (Lossy) Vector Addition Systems, based on the following ingredients: a rich assertional language based on the graph-based symbolic representation of upward-closed sets introduced in [DR00], the combination of the backward reachability algorithm of [ACJT96] lifted to the symbolic setting with a new heuristic rule based on structural properties of Petri Nets. We evaluate the method on several Petri Nets and parameterized systems taken from the literature [ABC+95,EM00,Fin93,MC99], and we compare the results with other finite and infinite-state verification tools.
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.
Download to read the full chapter text
Chapter PDF
References
ABC+95._M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. Series in Parallel Computing. John Wiley & Sons, 1995.
P. A. Abdulla and A. Nylén. Better is Better than Well: On Efficient Verification of Infinite-State Systems. In Proc. LICS 2000, pages 132–140, 2000.
P. A. Abdulla, K. Cerāns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS’ 96, pages 313–321, 1996.
T. Ball, S. Chaki, S. K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. MSR Technical Report 2000-116. In Proc. TACAS 2001, LNCS 2031, pages 158–173, 2001.
BLP+99._G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In Proc. CAV’ 99, LNCS 1633, pages 341–353, 1999.
B. Bérard and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmeti In Proc. CONCUR’ 99, LNCS 1664, pages 178–193, 1999.
A. Bouajjani, and R. Mayr. Model Checking Lossy Vector Addition Systems. In Proc. STACS’ 99, LNCS 1563, pages 323–333, 1999.
T. Bultan. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. In Proc. TACAS 2000, LNCS 1785, pages 441–455, 2000.
T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinitestate Systems using Presburger Arithmetics. In Proc. CAV’ 97, LNCS 1254, pages 400–411, 1997.
G. Chiola, G. Franceschinis, R. Gaeta, and M. Ribaudo. GreatSPN 1.7: Graphical Editor and Analyzer for Timed and Stochastic Petri Nets. Performance Evaluation, 24(1–2), pages 47–68, 1995.
G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proc. CAV 2000, LNCS 1855, pages 53–68, 1996.
G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proc. CSL’ 99, LNCS 1683, pag. 50–66, 1999.
G. Delzanno, and J. F. Raskin. Symbolic Representation of Upward-closed Sets. In Proc. TACAS 2000, LNCS 1785, pages 426–440, 2000.
E. A. Emerson and K. S. Namjoshi. On Model Checking for Nondeterministic Infinite-state Systems. In Proc. LICS’ 98, pages 70–80, 1998.
J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS’ 99, pages 352–359, 1999.
J. Esparza and S. Melzer. Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, 16:159–189, 2000.
A. Finkel. The minimal coverability graph for Petri nets. In In Advances in Petri Nets’ 93, LNCS 674, pages 210–243. Springer, 1993.
A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1–2):63–92, 2001.
S. M. German, A. P. Sistla. Reasoning about Systems with Many Processes. JACM 39(3): 675–735 (1992)
T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a Model Checker for Hybrid Systems. In Proc. CAV’ 97, LNCS 1254, pages 460–463, 1997.
KMM+97._Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In Proc. CAV’ 97, LNCS 1254, pages 424–435, 1997.
A. Miner, and G. Ciardo. Efficient Reachability Set Generation and Storage using Decision Diagrams. In Proc. of ICATPN’ 99, pages 6–25, 1999.
E. Pastor, J. Cortadella, M. A. Peña. Structural Methods to Improve the Symbolic Analysis of Petri Nets. In Proc. ICATPN’ 99, LNCS 1639, pages 26–45. Springer, 1999.
W. Reisig. Petri Nets. An introduction. EATCS Monographs on Theoretical Computer Science, Springer 1986.
M. Silva, E. Teruel, and J. M. Colom. Linear Algebraic and Linear Programming Techniques for Analysis of Place/Transition Net Systems. In W. Reisig and G. Rozenberg, editors. Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, LNCS 1491, pages 308–309. Springer, 1998.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delzanno, G., Raskin, JF., Van Begin, L. (2001). Attacking Symbolic State Explosion. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_28
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive