IEICE TRANSACTIONS on transactions
Verification and Synthesis of Concurrent Programs Using Petri Nets and Temporal Logic
Summary :
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.
- Publication
- IEICE TRANSACTIONS on transactions Vol.E73-E No.12 pp.2001-2010
- Publication Date
- 1990/12/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on the 3rd Karuizawa Workshop on Circuits and Systems)
- Category
- Graphs and Petri Nets
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Naoshi UCHIHIRA, Shinichi HONIDEN, "Verification and Synthesis of Concurrent Programs Using Petri Nets and Temporal Logic" in IEICE TRANSACTIONS on transactions,
vol. E73-E, no. 12, pp. 2001-2010, December 1990, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/transactions/10.1587/e73-e_12_2001/_p
Copy
@ARTICLE{e73-e_12_2001,
author={Naoshi UCHIHIRA, Shinichi HONIDEN, },
journal={IEICE TRANSACTIONS on transactions},
title={Verification and Synthesis of Concurrent Programs Using Petri Nets and Temporal Logic},
year={1990},
volume={E73-E},
number={12},
pages={2001-2010},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={December},}
Copy
TY - JOUR
TI - Verification and Synthesis of Concurrent Programs Using Petri Nets and Temporal Logic
T2 - IEICE TRANSACTIONS on transactions
SP - 2001
EP - 2010
AU - Naoshi UCHIHIRA
AU - Shinichi HONIDEN
PY - 1990
DO -
JO - IEICE TRANSACTIONS on transactions
SN -
VL - E73-E
IS - 12
JA - IEICE TRANSACTIONS on transactions
Y1 - December 1990
AB - 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.
ER -
English
