Efficient verification of parallel real-time systems

This paper presents an efficient model checking algorithm for one-safe time Petri nets and a timed temporal logic. The approach is based on the idea of (1) using only differences of timing variables to be able to construct a finite representation of the set of all reachable states and (2) further reducing the size of this representation by exploiting the concurrency in the net. This reduction of the state space is possible, because the considered linear-time temporal logic is stuttering invariant. The firings of transitions are only partially ordered by causality and a given formula; therefore the order of firings of independent transitions is irrelevant, and only one of several equivalent interleavings has to be generated for the evaluation of the given formula. In this paper the theory of timing verification with time Petri nets and temporal logic is presented, a concrete model checking algorithm is developed and proved to be correct, and some experimental results demonstrating the efficiency of the method are given.