Browse by author
Lookup NU author(s): Dr Victor Khomenko
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
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 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 holds.) In this paper a method for computing the shortest violation traces (which can greatly facilitate debugging) 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
Editor(s): Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E.
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Proceedings of the Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT)
Year of Conference: 2005
Pages: 141-155
Publisher: School of Computing Science, Newcastle University
URL: http://www.cs.ncl.ac.uk/publications/trs/abstract/915
