For the most recent entries see the Petri Nets Newsletter.

Branching Time Temporal Logic for Discrete Event System Analysis.

Passino, K.M.; Antsaklis, P.J.

In: Proceedings of the Twenty-Sixth Annual Allerton Conference on Communication, Control, and Computing, 1988, Monticello, IL, USA; Vol. 2, pages 1160-1169. Urbana, IL, USA: Univ. Illinois, 1988.

Abstract: Design specifications can be stated in a branching time temporal language and a verification algorithm can be used to test whether the specifications are true or not. In this paper, a certain Petri net is used to model finite state discrete event systems. It is shown that the Petri net model can be used to generate the structure over which the verification algorithm operates. Hence, the algorithm can be used to verify discrete event system properties that can be stated in a branching time temporal language. The approach to analysis is illustrated by three examples.

Keywords: branching time temporal logic; discrete event system; verification algorithm.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography