Difference between revisions of "Control design for hybrid systems with TuLiP: The temporal logic planning toolbox"

From MurrayWiki
Jump to: navigation, search
(update to final paper version)
Line 1: Line 1:
 
{{Paper
 
{{Paper
 
|Title=Control design for hybrid systems with TuLiP: The temporal logic planning toolbox
 
|Title=Control design for hybrid systems with TuLiP: The temporal logic planning toolbox
|Authors=Sumanth Dathathri, Ioannis Filippidis, Scott C. Livingston, Richard M. Murray, Necmiye Ozay
+
|Authors=Ioannis Filippidis, Sumanth Dathathri, Scott C. Livingston, Necmiye Ozay, Richard M. Murray
|Source=Submitted, 2016 IEEE Multi-Conference on Systems and Control (MSC)
+
|Source=2016 IEEE Multi-Conference on Systems and Control (MSC)
|Abstract=This tutorial describes TuLiP, the Temporal Logic Planning toolbox. TuLiP is a collection of tools for designing controllers for hybrid systems from specifications in temporal logic. The tools support a workflow that starts from a descrip- tion of desired behavior in temporal logic, and a description of the system to be controlled. The system can be represented as a discrete transition system, or a hybrid dynamical system with a mixed discrete and continuous state space. The system description can include both discrete and continuous uncontrollable variables that represent disturbances, communication signals, and other environmental factors that affect the system dynamics and controller decisions.
+
|Abstract=
 +
This tutorial describes TuLiP, the Temporal Logic Planning toolbox, a collection of tools for designing controllers
 +
for hybrid systems from specifications in temporal logic. The
 +
tools support a workflow that starts from a description of
 +
desired behavior, and of the system to be controlled. The
 +
system can have discrete state, or be a hybrid dynamical
 +
system with a mixed discrete and continuous state space. The
 +
desired behavior can be represented with temporal logic and
 +
discrete transition systems. The system description can include
 +
uncontrollable variables that take discrete or continuous values,
 +
and represent disturbances and other environmental factors
 +
that affect the dynamics, as well as communication signals that
 +
affect controller decisions.
  
For solving the control design problem, the logic specification is refined, by conjoining it with a discrete description of system dynamics in logic, which is an abstraction of the underlying continuous dynamics, in the case of hybrid systems. For piecewise affine dynamical systems, this abstraction is constructed automatically, guided by the geometry of the dynamics and under logical constraints from the specification. The resulting logic formulae describe admissible discrete behaviors that capture both controlled and environment variables. To find a controller, the toolbox solves a game of infinite duration. Existence of a discrete (winning) strategy for the controlled variables in this game is a proof certificate for the existence of a controller for the original problem that guarantees the satisfaction of the specification. This discrete strategy, refined with continuous controllers when needed, yields a feedback controller for the original hybrid system. The toolbox frontend is written in Python, with backends in C, Python and other languages.
+
A control design problem is solved in phases that involve
 +
abstraction, discrete synthesis, and continuous feedback control.
 +
Abstraction yields a discrete description of system dynamics in
 +
logic. For piecewise affine dynamical systems, this abstraction
 +
is constructed automatically, guided by the geometry of the dynamics
 +
and under logical constraints from the specification. The
 +
resulting logic formulae describe admissible discrete behaviors
 +
that capture both controlled and environment variables. The
 +
discrete description resulting from abstraction is then conjoined
 +
with the desired logic specification. To find a controller, the
 +
toolbox solves a game of infinite duration. Existence of a discrete
 +
(winning) strategy for the controlled variables in this game is a
 +
proof certificate for the existence of a controller for the original
 +
problem, which guarantees satisfaction of the specification. This
 +
discrete strategy, concretized by using continuous controllers,
 +
yields a feedback controller for the original hybrid system. The
 +
toolbox frontend is written in Python, with backends in C,
 +
Python, and Cython.
  
The tutorial starts with an overview of the theory behind TuLiP, and of its software architecture, organized into spec- ification frontends and backends that implement algorithms for abstraction, solving games, and interfaces to other tools. Then, the main elements for writing a specification for input to TuLiP are introduced. These include logic formulae, labeled transition systems, and hybrid dynamical systems, with linear or piecewise affine continuous dynamics. The working principles of the algorithms for predicate abstraction and discrete game solving using nested fixpoints are explained, by following the input specification through the various transformations that compile it to a symbolic representation that scales well to large games. The tutorial concludes with several design examples that demonstrate the toolbox’s capabilities.
+
The tutorial starts with an overview of the theory behind
|URL=http://www.cds.caltech.edu/~murray/preprints/dat+16-msc_s.pdf
+
TuLiP, and of its software architecture, organized into specifi-
 +
cation frontends and backends that implement algorithms for
 +
abstraction, solving games, and interfaces to other tools. Then,
 +
the main elements for writing a specification for input to TuLiP
 +
are introduced. These include logic formulae, discrete transition
 +
systems annotated with predicates, and hybrid dynamical systems,
 +
with linear or piecewise affine continuous dynamics. The
 +
working principles of the algorithms for predicate abstraction
 +
and discrete game solving using nested fixpoints are explained,
 +
by following the input specification through the various transformations
 +
that compile it to a symbolic representation that
 +
scales well to solving large games. The tutorial concludes
 +
with several design examples that demonstrate the toolbox’s
 +
capabilities.
 +
|URL=http://www.cds.caltech.edu/~ifilippi/pubs/2016_filippidis_msc.pdf
 
|Type=Conference paper
 
|Type=Conference paper
 
|ID=2016e
 
|ID=2016e
|Tag=dat+16-msc
+
|Tag=fil+16-msc
 
|Funding=SRC TerraSwarm
 
|Funding=SRC TerraSwarm
 
}}
 
}}

Revision as of 19:13, 3 October 2016

Title Control design for hybrid systems with TuLiP: The temporal logic planning toolbox
Authors Ioannis Filippidis, Sumanth Dathathri, Scott C. Livingston, Necmiye Ozay, Richard M. Murray
Source 2016 IEEE Multi-Conference on Systems and Control (MSC)
Abstract This tutorial describes TuLiP, the Temporal Logic Planning toolbox, a collection of tools for designing controllers

for hybrid systems from specifications in temporal logic. The tools support a workflow that starts from a description of desired behavior, and of the system to be controlled. The system can have discrete state, or be a hybrid dynamical system with a mixed discrete and continuous state space. The desired behavior can be represented with temporal logic and discrete transition systems. The system description can include uncontrollable variables that take discrete or continuous values, and represent disturbances and other environmental factors that affect the dynamics, as well as communication signals that affect controller decisions.

A control design problem is solved in phases that involve abstraction, discrete synthesis, and continuous feedback control. Abstraction yields a discrete description of system dynamics in logic. For piecewise affine dynamical systems, this abstraction is constructed automatically, guided by the geometry of the dynamics and under logical constraints from the specification. The resulting logic formulae describe admissible discrete behaviors that capture both controlled and environment variables. The discrete description resulting from abstraction is then conjoined with the desired logic specification. To find a controller, the toolbox solves a game of infinite duration. Existence of a discrete (winning) strategy for the controlled variables in this game is a proof certificate for the existence of a controller for the original problem, which guarantees satisfaction of the specification. This discrete strategy, concretized by using continuous controllers, yields a feedback controller for the original hybrid system. The toolbox frontend is written in Python, with backends in C, Python, and Cython.

The tutorial starts with an overview of the theory behind TuLiP, and of its software architecture, organized into specifi- cation frontends and backends that implement algorithms for abstraction, solving games, and interfaces to other tools. Then, the main elements for writing a specification for input to TuLiP are introduced. These include logic formulae, discrete transition systems annotated with predicates, and hybrid dynamical systems, with linear or piecewise affine continuous dynamics. The working principles of the algorithms for predicate abstraction and discrete game solving using nested fixpoints are explained, by following the input specification through the various transformations that compile it to a symbolic representation that scales well to solving large games. The tutorial concludes with several design examples that demonstrate the toolbox’s capabilities.

Type Conference paper
URL http://www.cds.caltech.edu/~ifilippi/pubs/2016_filippidis_msc.pdf
Tag fil+16-msc
ID 2016e
Funding SRC TerraSwarm
Flags