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 wi th each other to accomplish its own goal. This paper describes the aut omatic synthesis of a CDES from a modular temporal logic specification . First, MPTS (Modular Practical Temporal Specification language) is p roposed in which the new features (modular structure and domain specif ication) are appended to temporal logic. To overcome the "state explos ion problem", which occurs in generating a global automaton in former synthesis methods using temporal logic, a compositional synthesis is p roposed where automata are reduced at every composition step.