Computer aided verification (CAV) can be used to produce interesting benchmarks. In the bounded model checking approach to CAV we are given a finite state system, a (temporal) property and a bound n. The task is to check whether the property holds for the system by examining all execution sequences of at most n steps and to find a "counter execution" of length at most n if such exists.  A counter execution is a sequence of steps of the system that violates the property.

Here deadlock detection of 1-safe place/transition nets is put forward as a benchmark. Deadlock freedom is a typical property to be verified in a finite state system. A deadlock is a state of the system which does not have any successor states. Petri nets provide a way modelling finite state systems and 1-safe place/transition nets are a simple class of Petri nets which generalizes communicating automata.

INPUT: 1-safe place/transition net and an execution bound n (integer).

OUTPUT: An execution sequence of at most n transitions leading from the initial marking of the net to a deadlock marking if such a sequence exists and otherwise indication that no such sequence exists.

DATA SETS:

Deadlock detection test cases

NOTES:

1. Information on Petri nets and on place/transition nets can be found, e.g., in: J. Desel and W. Reisig. Place/Transition Petri nets. In Lectures on Petri Nets I: Basic Models, pages 122-173. Springer-Verlag, 1998.
2. An example of solving bounded deadlock checking problems using normal logic programs with stable models is described in: K. Heljanko and I. Niemel\"a. Answer set programming and bounded model checking. In Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning, pages 90-96, Stanford, USA, March 2001. AAAI Press.
3. The deadlock test cases described in the paper are available at http://www.tcs.hut.fi/~kepa/experiments/ASP2001/