A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications

DOI10.1109/TAC.2007.914952zbMath1367.93202OpenAlexW2150335178MaRDI QIDQ4974124

Calin Belta, Marius Kloetzer

Publication date: 8 August 2017

Published in: IEEE Transactions on Automatic Control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1109/tac.2007.914952

Mathematics Subject Classification ID

Related Items (66)

Quantitative Model Checking for a Controller Design ⋮ Formal methods for robot motion planning with time and space constraints (extended abstract) ⋮ Multi-agent planning under local LTL specifications and event-based synchronization ⋮ LTL receding horizon control for finite deterministic systems ⋮ Stabhyli ⋮ Minimum Attention Controller Synthesis for Omega-Regular Objectives ⋮ Linear temporal logic vehicle routing with applications to multi-UAV mission planning ⋮ Finite abstractions with robustness margins for temporal logic-based control synthesis ⋮ Verification of agent navigation in partially-known environments ⋮ Abstraction-based synthesis for stochastic systems with omega-regular objectives ⋮ Time window temporal logic ⋮ Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications ⋮ Resource-aware networked control systems under temporal logic specifications ⋮ Linear temporal logic for hybrid dynamical systems: characterizations and sufficient conditions ⋮ Temporal logic guided safe model-based reinforcement learning: a hybrid systems approach ⋮ Monitoring of perception systems: deterministic, probabilistic, and learning-based fault detection and identification ⋮ Flow functions, control flow functions, and the reach control problem ⋮ Lyapunov-barrier characterization of robust reach-avoid-stay specifications for hybrid systems ⋮ Robust stutter bisimulation for abstraction and controller synthesis with disturbance ⋮ Optimal mixed discrete-continuous planning for linear hybrid systems ⋮ Model-based reinforcement learning for approximate optimal control with temporal logic specifications ⋮ Decentralized abstractions for multi-agent systems under coupled constraints ⋮ AROC ⋮ Least-violating control strategy synthesis with safety rules ⋮ Limited-information control of hybrid systems via reachable set propagation ⋮ Resilient synchronization in robust networked multi-agent systems ⋮ Learning nonlinear hybrid systems ⋮ Mining requirements from closed-loop control models ⋮ On the decidability of stability of hybrid systems ⋮ Lyapunov analysis of rigid body systems with impacts and friction via sums-of-squares ⋮ Hybrid control lyapunov functions for the stabilization of hybridsystems ⋮ A toolbox for simulation of hybrid systems in matlab/simulink ⋮ Zélus ⋮ State estimation for polyhedral hybrid systems and applications to the Godunov scheme ⋮ Observer design for a class of piecewise affine hybrid systems ⋮ Automated analysis of real-time scheduling using graph games ⋮ Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets ⋮ One-shot computation of reachable sets for differential games ⋮ Tracking differentiable trajectories across polyhedra boundaries ⋮ Flowpipe approximation and clustering in space-time ⋮ Bounded model-checking of discrete duration calculus ⋮ Optimal CPU allocation to a set of control tasks with soft real--time execution constraints ⋮ Safe schedulability of bounded-rate multi-mode systems ⋮ Compositional heterogeneous abstraction ⋮ Quantitative timed simulation functions and refinement metrics for real-time systems ⋮ Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems ⋮ Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems ⋮ Control design for specifications on stochastic hybrid systems ⋮ Rewarding probabilistic hybrid automata ⋮ Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata ⋮ Specification-guided controller synthesis for linear systems and safe linear-time temporal logic ⋮ Temporal logic model predictive control for discrete-time systems ⋮ Iterative temporal motion planning for hybrid systems in partially unknown environments ⋮ Reachability and stabilization of discrete-time affine systems with disturbances ⋮ An input–output simulation approach to controlling multi-affine systems for linear temporal logic specifications ⋮ A design of GPU-based quantitative model checking ⋮ Optimal control of multi-task Boolean control networks via temporal logic ⋮ Time-constrained temporal logic control of multi-affine systems ⋮ Optimization of Multi-agent Motion Programs with Applications to Robotic Marionettes ⋮ Computation of Discrete Abstractions of Arbitrary Memory Span for Nonlinear Sampled Systems ⋮ Sampling polynomial trajectories for LTL verification ⋮ Funnel control for fully actuated systems under a fragment of signal temporal logic specifications ⋮ Robust approximate symbolic models for a class of continuous-time uncertain nonlinear systems via a control interface ⋮ Constructive hybrid games ⋮ Safe and stabilizing distributed multi-path cellular flows ⋮ Robustly complete finite-state abstractions for verification of stochastic systems

This page was built for publication: A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications