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

DOI10.1016/j.automatica.2021.109723zbMath1478.93187OpenAlexW3166440625MaRDI QIDQ2665348

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

Publication date: 19 November 2021

Published in: Automatica (Search for Journal in Brave)

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

zbMATH Keywords

control synthesisabstractioncontroller constraints and structurecomputational issuesLTL specification

Mathematics Subject Classification ID

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

Related Items (1)

Robust stutter bisimulation for abstraction and controller synthesis with disturbance

Uses Software

• TuLiP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An implementation of an efficient algorithm for bisimulation equivalence
• Bisimilar linear systems.
• Augmented finite transition systems as abstractions for control synthesis
• Formal methods for discrete-time dynamical systems
• Verification and Control of Hybrid Systems
• Some tractable supervisory control problems for discrete-event systems modeled by Buchi automata
• Bisimulation equivalence of differential-algebraic systems
• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• A classification of symbolic transition systems
• An O ( m log n ) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation
• Approximation Metrics for Discrete and Continuous Systems
• Feedback Refinement Relations for the Synthesis of Symbolic Controllers
• Symbolic Models for Nonlinear Control Systems Without Stability Assumptions
• Synthesis of Reactive Switching Protocols From Temporal Logic Specifications

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