Wolf, Karsten and Wimmel, Harro - Applying CEGAR to the Petri Net State Equation

lmcs:1036 - Logical Methods in Computer Science, September 29, 2012, Volume 8, Issue 3
Applying CEGAR to the Petri Net State Equation

Authors: Wolf, Karsten and Wimmel, Harro

We propose a reachability verification technique that combines the Petri net state equation (a linear algebraic overapproximation of the set of reachable states) with the concept of counterexample guided abstraction refinement. In essence, we replace the search through the set of reachable states by a search through the space of solutions of the state equation. We demonstrate the excellent performance of the technique on several real-world examples. The technique is particularly useful in those cases where the reachability query yields a negative result: While state space based techniques need to fully expand the state space in this case, our technique often terminates promptly. In addition, we can derive some diagnostic information in case of unreachability while state space methods can only provide witness paths in the case of reachability.

DOI : 10.2168/LMCS-8(3:27)2012
Volume: Volume 8, Issue 3
Published on: September 29, 2012
Submitted on: October 15, 2011
Keywords: Computer Science - Logic in Computer Science,Computer Science - Data Structures and Algorithms,F.2.2, I.6.4


Consultation statistics

This page has been seen 165 times.
This article's PDF has been downloaded 238 times.