LTLCon:
Software for control of linear systems
from LTL formulas over
linear predicates
Authors: Marius Kloetzer and Calin Belta
Center for Information and
Systems Engineering
Boston University
{kmarius,cbelta}@bu.edu
Problem formulation: Consider the following affine control system
in a full dimensional polytope PN
in RN:
(1)
where 
, 
, 
, and 
is a given polyhedral
subset of Rm capturing
control constraints. Let 
be an
formula over a set of
atomic propositions given as arbitrary strict linear inequalities in RN:
(2)
where 
and 
.
LTLCon finds sets of initial states and feedback control strategies for system
(1) so that all trajectories of the corresponding closed loop system satisfy , while always staying inside 
.
An exact definition of semantics of LTL formulas over trajectories of
the system can be found in [4,5]. Intuitively, a
trajectory of (1) satisfies a formula if the word of satisfied predicates
produced by the evolving trajectory satisfies the formula in the classical way
defined in temporal logic. Some illustrative examples of words defined by
continuous trajectories are given in Figure 1, where 
, 
are open half-spaces
and 
, 
, 
, 
, 
, 
. Continuous trajectory 
starts from the region
where the predicates in 
are true and converges
to a point in the region where the predicates in 
are true. The word 
is 
. Trajectory 
starts from and loops infinitely
as shown in the figure. The corresponding word 
will be 
. For trajectory 
originating in and converging inside , the word 
is 
. Finally, trajectory 
, which has a self-intersection, generates the word 
.
1. Examples of
continuous trajectories
Implementation notes and
acknowledgements: LTLCon is implemented in Matlab. Even
though this is transparent to the user, LTLCon also
uses two free packages. The first one is a mex-file
calling CDD in Matlab [1] and it is used to convert a
polytope from V to H representations and vice-versa. The second one is LTL2BA
[2], which is used to convert an LTL formula to a Büchi automaton.
Usage and download: LTLCon takes as
input the polytope , the matrices 
, 
, and 
of system, and the LTL
formula . If it finds a solution, it plots the produced trajectories
corresponding to user defined initial states. Download LTLCon
from here. If you use our
script files, please cite reference [3] from below.
Example produced using LTLCon:
Consider the following system:
(3)
Polytope 
is specified in H form
(
), as the intersection of 8 closed half spaces, defined by: 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
. Control constraints are captured by the set
.
We define a set 
containing 10
predicates, as in equation (2), where: 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
, 
.
Figure 2 depicts the bounding polytope , the vector field given by the drift of system (3), the
predicates , 
, and the corresponding feasible subpolytopes
(labeled 
, 
).
2. The arrows
represent the drift vector field of system (3). The yellow boxes mark the
half-spaces corresponding to atomic propositions , . The regions to
be visited are green, while the obstacles are gray.
We have chosen an LTL formula inspired from robot motion planning, which
involves visiting a sequence of three regions infinitely often, while always
avoiding three obstacles. The regions to be visited are, in order: 
, 
and 
, where 
denotes the set of all
points in the interior of the polytope with label . The obstacles are
represented by the polyhedral regions 
, 
and 
. All regions to be visited and obstacles are represented in
Figure 2. The LTL formula can be written as 
. By expressing interesting regions 
and 
, 
in terms of predicates
, 
we obtain 
.
The set of initial states from which there exist continuous trajectories
satisfying the formula is the union of the yellow polytopes in Figure 3 (a). A
continuous trajectory starting from 
(blue diamond) is also
shown in Figure 3 (b).
|
|
|
|
(a) |
(b) |
3. (a) The set of initial states from which there exist
continuous trajectories satisfying formula . (b) An example
of such a trajectory.
References:
[1] Torrisi, F., Baotic,
M.: Matlab interface for the cdd
solver. (URL http://control.ee.ethz.ch/ hybrid/cdd.php)
[2] Gastin, P., Oddoux, D.: Fast LTL to Büchi
automata translation. In G. Berry, H.C., Finkel,
A., eds.: Proceedings of the 13th Conference on Computer Aided Verification
(CAV’01). Number 2102 (2001) 53–65
[3] Kloetzer,
M., Belta, C.: A fully automated
framework for control of linear systems from LTL specifications. In: Lecture Notes in Computer Science, Springer Berlin / Heidelberg,
vol. 3927, pp. 333 – 347, 2006.
[4] Kloetzer,
M., Belta, C.: A fully automated
framework for controller synthesis from linear temporal logic specifications.
Technical Report CISE 2005-IR-0050, Boston University (2005)
http://www.bu.edu/systems/research/publications/2005/2005-IR-0050.pdf.