In: Lecture Notes in Computer Science, Vol. 1684: Fundamental of Computation Theory, pages 547-558. Springer-Verlag, 1999.
Abstract: The intention of the paper is to develop an efficient model checker for real-time systems represented by safe time Petri nets and the real-time branching-time temporal logic TCTL. The method is based on the idea of (i) using the known region graph technique to construct a finite representation of the state-space of a time Petri net, and (ii) further reducing the size of this representation by exploiting the net concurrency. To show the correctness of the reduction, a notion of timed stuttering equivalence is introduced. Some experimental results which demonstrate the efficiency of the method are also given.
Keywords: TCTL, branching-time temporal logic, model checking, partial orders, time Petri nets, timed stuttering equivalence.