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.
