Attacking Symbolic State Explosion in Parameterized Verification

Giorgio Delzanno, Jean-Francois Raskin, and Laurent Van Begin

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001

Abstract

We propose a new symbolic model checking algorithm for parameterized concurrent systems modeled as Petri Nets, Vector Addition Systems, Lossy Vector Addition Systems, based on the following ingredients: (1) a {\em rich assertional language} based on the {\em graph-based} symbolic representation of upward-closed sets introduced in \cite{DR00}, (2) the combination of the {\em backward reachability algorithm} of \cite{ACJT96} lifted to the symbolic setting with a {\em new heuristics} based on {\em structural properties} of Petri Nets. We evaluate the method on several parameterized examples taken from the literature, and we compare the results with other finite and infinite-state verification tools. Ref: \bibitem[ACJT96]{ACJT96} P.~A.~Abdulla, K.~{C}er{\=a}ns, B.~Jonsson and Y.-K.~Tsay. \newblock General Decidability Theorems for Infinite-State Systems. \newblock In {\em Proc. 10th IEEE Int. Symp. on Logic in Computer Science}, pages 313--321, 1996. \bibitem[DR00]{DR00} G.~Delzanno, and J.~F.~Raskin. \newblock Symbolic Representation of Upward-closed Sets. \newblock In {\em Proc. TACAS 2000}, LNCS 1785, pages 426-440, 2000.

 Server START Conference Manager Update Time 28 Mar 2001 at 08:36:01 Maintainer www-cav01@lsv.ens-cachan.fr.
 Conference Systems