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

Naoshi UCHIHIRA  Shinichi HONIDEN  

IEICE TRANSACTIONS (1976-1990)   Vol.E73   No.12   pp.2001-2010
Publication Date: 1990/12/25
Online ISSN: 
Print ISSN: 0000-0000
Type of Manuscript: Special Section PAPER (Special Issue on the 3rd Karuizawa Workshop on Circuits and Systems)
Category: Graphs and Petri Nets

Full Text: PDF(860.1KB)
>>Buy this Article

Both Petri nets and temporal logic have been widely used to specify concurrent programs. Petri nets appropriate to specify the behavioral structures of programs explicitly, while temporal logic is appropriate to specify the properties and constraints of programs. Since one can complement the other, using a combination of Petri nets and temporal logic is a highly promising approach to analyze, verify and synthesize concurrent programs. For the purpose of automatic program verification and synthesis, the emptiness problem (i.e., wheter a legal firing transition sequence satisfying a given temporal logic formula on a given Petri net exists) must be decidable. This paper reports a class to combine Petri nets and temporal logic as an infinite language and whose emptiness problem is decidable. We then show how to verify concurrent programs, using Petri nets and temporal logic, and also propose a compositional synthesis method that tune up reusable program components to satisfy a temporal logic specification.