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


IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E75-A   No.3   pp.380-391
Publication Date: 1992/03/25
Online ISSN: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on the 4th Karuizawa Workshop on Circuits and Systems)
cooperating discrete event system,  temporal logic,  compositional program synthesis,  state explosion problem,  

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

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.