Linear-time temporal logic control of discrete event models of cooperative robots

Abstract

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.