Compositional Synthesis for Cooperating Discrete Event Systems from Modular Temporal Logic Specifications

Naoshi UCHIHIRA

Compositional Synthesis for Cooperating Discrete Event Systems from Modular Temporal Logic Specifications

Naoshi UCHIHIRA

Full Text Views

0

Share
Cite this

Summary :

A Discrete Event System (DES) is a system that is modeled by a finite automaton. A Cooperating Discrete Event System (CDES) is a distributed system which consists of several local DESs which are synchronized with each other to accomplish its own goal. This paper describes the automatic synthesis of a CDES from a modular temporal logic specification. First, MPTS (Modular Practical Temporal Specification language) is proposed in which the new features (modular structure and domain specification) are appended to temporal logic. To overcome the "state explosion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is proposed where automata are reduced at every composition step.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E75-A No.3 pp.380-391

Publication Date: 1992/03/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Section on the 4th Karuizawa Workshop on Circuits and Systems)

Category

Cite this

Copy

Naoshi UCHIHIRA, "Compositional Synthesis for Cooperating Discrete Event Systems from Modular Temporal Logic Specifications" in IEICE TRANSACTIONS on Fundamentals, vol. E75-A, no. 3, pp. 380-391, March 1992, doi: .
Abstract: A Discrete Event System (DES) is a system that is modeled by a finite automaton. A Cooperating Discrete Event System (CDES) is a distributed system which consists of several local DESs which are synchronized with each other to accomplish its own goal. This paper describes the automatic synthesis of a CDES from a modular temporal logic specification. First, MPTS (Modular Practical Temporal Specification language) is proposed in which the new features (modular structure and domain specification) are appended to temporal logic. To overcome the "state explosion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is proposed where automata are reduced at every composition step.
URL: https://globals.ieice.org/en_transactions/fundamentals/10.1587/e75-a_3_380/_p

Copy

@ARTICLE{e75-a_3_380,
author={Naoshi UCHIHIRA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Compositional Synthesis for Cooperating Discrete Event Systems from Modular Temporal Logic Specifications},
year={1992},
volume={E75-A},
number={3},
pages={380-391},
abstract={A Discrete Event System (DES) is a system that is modeled by a finite automaton. A Cooperating Discrete Event System (CDES) is a distributed system which consists of several local DESs which are synchronized with each other to accomplish its own goal. This paper describes the automatic synthesis of a CDES from a modular temporal logic specification. First, MPTS (Modular Practical Temporal Specification language) is proposed in which the new features (modular structure and domain specification) are appended to temporal logic. To overcome the "state explosion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is proposed where automata are reduced at every composition step.},
keywords={},
doi={},
ISSN={},
month={March},}

Copy

TY - JOUR
TI - Compositional Synthesis for Cooperating Discrete Event Systems from Modular Temporal Logic Specifications
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 380
EP - 391
AU - Naoshi UCHIHIRA
PY - 1992
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E75-A
IS - 3
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - March 1992
AB - A Discrete Event System (DES) is a system that is modeled by a finite automaton. A Cooperating Discrete Event System (CDES) is a distributed system which consists of several local DESs which are synchronized with each other to accomplish its own goal. This paper describes the automatic synthesis of a CDES from a modular temporal logic specification. First, MPTS (Modular Practical Temporal Specification language) is proposed in which the new features (modular structure and domain specification) are appended to temporal logic. To overcome the "state explosion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is proposed where automata are reduced at every composition step.
ER -