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.
Deadlock detection test cases