Browse by author
Lookup NU author(s): Dr Victor Khomenko
Model checking based on the causal partial order semantics of Petri nets is an approach widely applied to cope with the state space explosion problem. One of the ways to exploit such a semantics is to consider (finite prefixes of) net unfoldings - themselves a class of acyclic Petri nets - which contain enough information, albeit implicit, to reason about the reachable markings of the original Petri nets. One of the possibilities for the verification process is to build a finite and complete prefix and use it for constructing a Boolean formula such that any satisfying assignment to its variables yields a trace violating the property being checked. (And if there are no satisfying assignments then the property is not violated.) In this paper a method for computing the shortest violation traces (which can greatly facilitate debugging the system) is proposed. Experimental results demonstrate that it can achieve significant reductions in the size of the Boolean formula as well as in the time required to compute a shortest violation trace, when compared with a naive approach.
Author(s): Khomenko V
Publication type: Report
Publication status: Published
Series Title: School of Computing Science Technical Report Series
Year: 2004
Pages: 17
Print publication date: 01/04/2004
Source Publication Date: April 2004
Report Number: 841
Institution: School of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: http://www.cs.ncl.ac.uk/publications/trs/papers/841.pdf
