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

lmcs:1036 - Logical Methods in Computer Science, September 29, 2012, Volume 8, Issue 3 - https://doi.org/10.2168/LMCS-8(3:27)2012
Applying CEGAR to the Petri Net State EquationArticle

Authors: Karsten Wolf ; Harro Wimmel

    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.


    Volume: Volume 8, Issue 3
    Published on: September 29, 2012
    Imported on: October 15, 2011
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Data Structures and Algorithms,F.2.2, I.6.4

    11 Documents citing this article

    Consultation statistics

    This page has been seen 1534 times.
    This article's PDF has been downloaded 501 times.