Efficient verification of parallel real-time systems

Abstract

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, i.e. only one of several equivalent interleavings being generated for the evaluation of the given formula. This reduction of the state space is possible, because the considered linear-time temporal logic is stuttering invariant. In this paper the concrete model checking algorithm is developed and some experimental results which demonstrate the efficiency of the method are given.