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.
Cite
CITATION STYLE
Delzanno, G., Raskin, J. F., & Van Begin, L. (2001). Attacking symbolic state explosion. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2102, pp. 298–310). Springer Verlag. https://doi.org/10.1007/3-540-44585-4_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
