Model checking based on prefixes of petri net unfoldings

摘要

The human society is becoming increasingly dependent on automated control systems, and the correct behaviour and reliability of the hardware and software used to implement them is often of a paramount importance. Yet, the growing complexity of such system makes it hard to design them without defects. Especially difficult is the development of concurrent systems, because they are generally harder to understand, and errors in them often do not show up during the testing. Therefore, the conventional methods are not sufficient for establishing the correctness of such systems, and some kind of computer-aided formal verification is required. One of the most popular formal verification techniques is model checking, in which the verification of a system is carried out using a finite representation of its state space. While being convenient in practice, it suffers a major drawback, viz. the state space explosion problem. That is, even a relatively small system specification can (and often does) yield a very large state space. To alleviate this problem, a number of methods have been proposed. Among them, a prominent technique is McMillan's (finite prefixes of) Petri net unfoldings. It relies on the partial order view of concurrent computation, and represents system states implicitly, using an acyclic net, called a prefix. Often such prefixes are exponentially smaller than the corresponding reachability graphs, especially if the system at hand exhibits a lot of concurrency. This thesis is all about efficient verification based on this technique. It discusses the theory of finite and complete prefixes of Petri net unfoldings and provides several practical verification algorithms. On one hand, the thesis addresses the issue of efficient prefix generation, suggesting a new method of computing possible extensions of a branching process, a parallel unfolding algorithm, and an unfolding algorithm for a class of highlevel Petri nets. On the other hand, it shows how unfolding prefixes can be used for practical verification, proposing a new integer programming verification technique. This technique can be used to check many fundamental properties, such as deadlock freeness, mutual exclusion, reachability and coverability of a marking, and extended reachability. Moreover, it can be applied to check state encoding properties of specifications of asynchronous circuits, yielding a fast and memory-efficient algorithm.