LTLCon

LTLCon

Description: We consider the following problem: given a linear system x=Ax+b+Bu with polyhedral control constraints U, and given an arbitrary LTL_X formula f over an arbitrary set of linear predicates, find initial states and a feedback control strategy u so that the corresponding trajectories of the closed loop system verify the formula f, whilestaying inside a given full-dimensional polytope PN.

Our approach to solving the above problem can be summarized as the following three steps. In the first step, we construct a finite state "generator" transition system T_g. Its states are the equivalence classes produced by the feasible full-dimensional subpolytopes of PN determined by the linear predicates appearing in the formula f. The transitions of T_g are determined by adjacency of subpolytopes and existence of feedback controllers making such subpolytopes invariant or driving all states in a subpolytope to an adjacent subpolytope through a common facet. In the second step, we produce runs of T_g that satisfy formula f. This is in essence a model checking problem, and we use standard tools based on B uchi automata. In the third step, we construct a feedback "control strategy", which leads to a closed loop hybrid system, whose continuous trajectories satisfy formula f. We implemented our approach as a user friendly software package LTLCon under Matlab

VO Integration: No

Active: No

Available Benchmarks: No

Website: http://sites.bu.edu/hyness/ltl-control/

Download: Link

Documentation: See webpage.

Contact: Marius Kloetzer and Calin Belta

Excerpt from: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.90.7507&rep=rep1&type=pdf