Abstract
A systematic way of analyzing and synthesizing supervised discrete event systems using temporal logic is proposed. Syntax and semantics of temporal logic that are suitable for the study of supervised discrete-event systems are introduced. A systematic way is given to verify that a temporal logic formula is satisfied in a supervised discrete-event system. Given a temporal logic formula, a supervised discrete-event system satisfying the formula is synthesized. A synthesis algorithm is developed. The development is illustrated by examples

This publication has 7 references indexed in Scilit: