COMPOSITIONAL SYNTHESIS FOR COOPERATING DISCRETE EVENT SYSTEMS FROM MODULAR TEMPORAL LOGIC SPECIFICATIONS

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.