Applying CEGAR to the Petri Net State Equation

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...

Full description

Bibliographic Details
Main Authors: Karsten Wolf, Harro Wimmel
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2012-09-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/1036/pdf