For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Verification and Synthesis of Concurrent Programs Using Petri Nets and Temporal Logic
Naoshi UCHIHIRA Shinichi HONIDEN
IEICE TRANSACTIONS (1976-1990)
Publication Date: 1990/12/25
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.