Temporal
Logic Control of Continuous Systems
University
of Pennsylvania
Department
of Electrical and Systems Engineering
Emebbeded
systems, which merge information systems with physical systems, are ubiquitous.
Computational systems operating in parallel with dynamical or control systems
give rise to tremendous modeling and design challenges for the modern
engineer. On one hand,
control theory has historically focused on properties such as stability,
controllability, and optimality. Advances in control theory usually focused on
the complexity of the model, but
not the complexity of the specification. Embedded systems require very novel, very challenging
specifications that have to deal with synchronization, sequencing, and temporal
ordering of different tasks.
Mathematically formulating such desired specifications cannot be
naturally described using traditional formulations in control theory. On the other hand, concurrency theory
and formal verification have popularized the use of several temporal logics
such as Linear Temporal Logic (LTL), and Computation Tree Logic (CTL) to
describe such complex specifications. However, the emphasis has been on
verification of these properties for purely discrete systems, and not on synthesis
for systems with a continuous component.
In this
talk, I will present an algorithmic approach for automatically synthesizing
hybrid controllers for continuous systems in order to satisfy specifications
that are expressed in temporal logics. In particular, given a controllable
linear system, and a finite set of predicates in a special form, we present an
algorithm that extracts a property-dependent, finite abstraction which is
equivalent (bi-similar) to the original control systems. This enables the use of
algorithmic procedures for controller synthesis based on powerful automata
theoretic and discrete-event techniques, bridging a semantic gap between
control theoretic models and computer science specifications. The discrete controllers
for the abstracted model are then formally refined to hybrid controllers for
the original control system that are formally correct by construction. A Matlab implementation receives as
inputs a control system, the temporal logic formula, and automatically generates
a StateFlow/Simulink supervisor.
This is
joint work with Paulo Tabuada and George Fainekos.
3:30 – 4:30
p.m.