SCCSyn: Controller Synthesis for Discrete-Time Linear Systems from scLTL specifications

Introduction

This toolbox is designed to synthesize controllers for discrete-time linear systems from specifications given as formulas of syntactically co-safe linear temporal logic over linear predicates in the state variables of the system. The toolbox takes as input a scLTL formula over a set of linear predicates, the matrices of discrete-time linear system, and the control constraints set, and produces maximal set of initial states and feedback controllers such that the trajectories of the closed-loop system originating from the identified set of initial states satisfy the given formula. The toolbox uses scheck tool to construct a finite state automaton for a given scLTL formula. The control synthesis part is implemented in MATLAB and MPT Toolbox is used for polyhedral operations. The MATLAB toolbox implements a systematic procedure for the automatic computation of sets of initial states and feedback controllers such that all the resulting trajectories of the corresponding closed-loop system satisfy the given specifications. The procedure is based on the iterative construction and refinement of an automaton that enforces the satisfaction of the formula. Interpolation and polyhedral Lyapunov function based approaches are implemented to compute the polytope-to-polytope controllers that label the transitions of the automaton.

Download

download SCCSyn

Dependencies

MPT Toolbox (Polyhedral operations)
lbt2dot (Automata to graph translation for visualization)
scheck (scLTL to FSA conversion)
An newer version of scheck is used for computation. The version is updated by Dr. Amit Bhatia and included in the package provided.