**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 *P _{N}* in

*:*

**R**^{N}_{}

^{(1)}

where

_{},

_{},

_{}, and

_{}is a given polyhedral subset of

**capturing control constraints. Let**

*R*^{m}_{}be an

_{}formula over a set of atomic propositions given as arbitrary strict linear inequalities in

*R**:*

^{N}_{}

^{(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 [3],[4]. 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 _{}.

Fig.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.

_{}, the matrices _{ }, _{}, and _{} of a 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 _{}, _{}).

Fig.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) |

Fig.3. 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.

[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).