LanGuiCS-MPC
LanGuiCS: Language-Guided Controller Synthesis
Description
This toolbox is designed to synthesize controllers for discrete-time piece-wise affine (PWA) systems from specifications given as formulas of syntactically co-safe linear temporal logic (csLTL) 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 a PWA system, control constraints sets and operating regions, 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 set contraction based approaches are implemented to compute the polytope-to-polytope controllers that label the transitions of the automaton. The toolbox allows for displaying the set of initial states and simulating trajectories of the closed-loop system for 2D and 3D examples.
Download
Dependencies
MPT Toolbox (Polyhedral operations)
lbt2dot (Automata to graph translation for visualization)
scheck (scLTL to FSA conversion)
A newer version of scheck is used for computation. The version is updated by Dr. Amit Bhatia and included in the package provided.
LanGuiMPC: Language-Guided Model Predictive Control
Description
This toolbox is an extension of the LanGuiCS toolbox. The main Matlab function implements an MPC controller for a discrete time piece-wise affine system constrained to satisfy a temporal logic specification over a set of linear predicates in its state variables. The cost is a quadratic function that penalizes the distance from desired state and control trajectories, which are assumed to be observable for a finite time horizon. The specification is a formula of syntactically co-safe Linear Temporal Logic (scLTL), which can be satisfied in finite time. The MPC controller solves a set of convex optimization problems guided by the specification and subject to progress constraints. The constraints are implemented with respect to the control strategy produced by LanGuiCS. This toolbox plots the closed loop trajectories for 2D and 3D examples, and stores computation summaries in a file.
Download
Download LanGuiMPC
(Includes all dependent packages from LanGuiCS)
LanGuiMPC_v2: Language- Guided Model Predictive Control
Description
The new toolbox LanGuiMPC_v2 extends the previous version in two main directions. First, the terminal constraint approach (also implemented in the previous version) is updated. In particular, the constraints of the optimization problem are relaxed. Second, the new version implements a terminal cost approach for enforcing the satisfaction of the specification. The new toolbox uses Gurobi for solving linear and quadratic programming problems.
