Linear-time temporal logic control of discrete event models of cooperative robots
Bruno Lacerda, Pedro U. Lima · Journal of Physical Agents (JoPha) · 2008
A Discrete Event System (DES) is a discrete state space dynamic system that evolves in accordance with the instantaneous occurrence, at possibly unkown times, of physical events.Given a DES, its behavior (the sequence of displayed events) may not satisfy a set of logical performance objectives.The purpose of Supervisory Control is to restrict that behavior in order to achieve those objectives.Linear-Time Temporal Logic (LTL) is an extension of Propositional Logic which allows reasoning over an infinite sequence of states.We will use this logical formalism as a way to specify our performance objectives for a given DES and build a supervisor that restricts the DES' behavior to those objectives by construction.Several simulated application examples illustrate the developed method.