For the most recent entries see the Petri Nets Newsletter.

Verification and Synthesis of Concurrent Programs Using Petri Nets and Temporal Logic.

Uchihira, N.; Honiden, S.

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.

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

Back to the Petri Nets Bibliography