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.