Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications

DOI10.1016/J.AUTOMATICA.2021.109723MaRDI QIDQ2665348zbMATH OpenOpenAlexFDO

Authors Sahar Mohajerani, Robi Malik, Andrew Wintenberg, Stéphane Lafortune, Necmiye Ozay

Publication date 19 November 2021

Published in Automatica (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1016/j.automatica.2021.109723

zbMATH Keywords

abstractioncontrol synthesiscontroller constraints and structurecomputational issuesLTL specification

Mathematics Subject Classification ID

Synthesis problems (93B50) Temporal logic (03B44)

Recommendations

• An input-output simulation approach to controlling multi-affine systems for linear temporal logic specifications
• Synthesis using approximately bisimilar abstractions, state-feedback controllers for safety specifications
• Duality-based nested controller synthesis from STL specifications for stochastic linear systems
• Reactive synthesis from signal temporal logic specifications
• Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\)

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 177845 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• A classification of symbolic transition systems
• An \(\mathcal O(m\log n)\) algorithm for computing stuttering equivalence and branching bisimulation
• An implementation of an efficient algorithm for bisimulation equivalence
• Approximation Metrics for Discrete and Continuous Systems
• Augmented finite transition systems as abstractions for control synthesis
• Bisimilar linear systems.
• Bisimulation equivalence of differential-algebraic systems
• Feedback Refinement Relations for the Synthesis of Symbolic Controllers
• Formal methods for discrete-time dynamical systems
• Some tractable supervisory control problems for discrete-event systems modeled by Buchi automata
• Symbolic Models for Nonlinear Control Systems Without Stability Assumptions
• Synthesis of Reactive Switching Protocols From Temporal Logic Specifications
• Verification and Control of Hybrid Systems

Cited in

(2)

• An input-output simulation approach to controlling multi-affine systems for linear temporal logic specifications
• Robust stutter bisimulation for abstraction and controller synthesis with disturbance

Describes a project that uses

Uses Software

• TuLiP

This page was built for publication: Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2665348)