In: Transactions of the Institute of Electronics, Information and Communication Engineers E, Vol. E73, No. 12, pages 2001-2010. December 1990.
Abstract: Using a combination of Petri nets and temporal logic is a promising approach to analyze, verify and synthesize concurrent programs. For the purpose of automatic program verification and synthesis, the emptiness problem (i.e. whether a legal firing transition sequence satisfying a given temporal logic formula on a given Petri net exists) must be decidable. This paper reports a combination of Petri nets and temporal logic as an infinite language whose emptiness problem is decidable. The authors then show how to verify concurrent programs, and also propose a compositional synthesis method that tunes up reusable program components to satisfy a temporal logic specification.
Keywords: verification (and) synthesis (of) concurrent program(s) (using nets and) temporal logic; automatic program verification; emptiness problem decidability; compositional synthesis; reusable program component.