State machines, temporal logic and control: A framework for discrete event systems

A framework is proposed for investigating the verification and synthesis of controllers for real-time discrete event systems. In the framework, plants and controllers are modelled with extended state machines (ESMs), and a real-time temporal logic (RTL) is used for specification of required plant behaviour and for verifying that controllers satisfy their specifications. Controllers are implemented as tasks in a real-time distributed programming language. This paper discusses the issues of modelling and specification.