A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
Top Cited Papers
- 31 March 2008
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Automatic Control
- Vol. 53 (1), 287-297
- https://doi.org/10.1109/tac.2007.914952
Abstract
We consider the following problem: given a linear system and a linear temporal logic (LTL) formula over a set of linear predicates in its state variables, find a feedback control law with polyhedral bounds and a set of initial states so that all trajectories of the closed loop system satisfy the formula. Our solution to this problem consists of three main steps. First, we partition the state space in accordance with the predicates in the formula, and construct a transition system over the partition quotient, which captures our capability of designing controllers. Second, using a procedure resembling model checking, we determine runs of the transition system satisfying the formula. Third, we generate the control strategy. Illustrative examples are included.Keywords
This publication has 30 references indexed in Scilit:
- A control problem for affine dynamical systems on a full-dimensional polytopeAutomatica, 2004
- Bisimilar linear systemsAutomatica, 2003
- Physical Traces: Quantum vs. Classical Information ProcessingElectronic Notes in Theoretical Computer Science, 2003
- Fast LTL to Büchi Automata TranslationLecture Notes in Computer Science, 2001
- O-Minimal Hybrid SystemsMathematics of Control, Signals, and Systems, 2000
- Automata-Theoretic Approach to Planning for Temporally Extended GoalsLecture Notes in Computer Science, 2000
- Proving properties of continuous systems: qualitative simulation and temporal logicArtificial Intelligence, 1997
- The algorithmic analysis of hybrid systemsTheoretical Computer Science, 1995
- A theory of timed automataTheoretical Computer Science, 1994
- A note on two problems in connexion with graphsNumerische Mathematik, 1959