Robust stutter bisimulation for abstraction and controller synthesis with disturbance

DOI10.1016/J.AUTOMATICA.2023.111394MaRDI QIDQ6152513zbMATH OpenFDO

Authors Jonas Krook, Robi Malik, Sahar Mohajerani, M. Fabian

Publication date 13 February 2024

Published in Automatica (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2205.13959

zbMATH Keywords

abstractioncontroller synthesiscyber-physical systemsdisturbanceslinear temporal logic

Mathematics Subject Classification ID

Synthesis problems (93B50) Networked control (93B70) Perturbations in control/observation systems (93C73) Control/observation systems involving computers (process control, etc.) (93C83)

Abstract: This paper proposes a method to synthesise controllers for cyber-physical systems such that the controlled systems satisfy specifications given as linear temporal logic formulas. The focus is on systems with disturbance, where future states cannot be predicted exactly due to uncertainty in the environment. The approach used to solve this problem is to first construct a finite-state abstraction of the original system and then synthesise a controller for the abstract system. For this approach, the robust stutter bisimulation relation is introduced, which preserves the existence of controllers for any given linear temporal logic formula. States are related by the robust stutter bisimulation relation if the same target sets can be guaranteed to be reached or avoided under control of some controllers, thereby ensuring that disturbances have similar effect on paths that start in related states. This paper presents an algorithm to construct the corresponding robust stutter bisimulation quotient to solve the abstraction problem, and it is shown, by explicit construction, that there exists a controller enforcing a linear temporal logic formula for the original system if and only if a corresponding controller exists for the quotient system. Lastly, the result of the algorithm and the controller construction are demonstrated by application to an example of robot navigation.

Recommendations

• Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications
• Robust abstractions for control synthesis: completeness via robustness for linear-time properties
• Abstraction, discretization, and robustness in temporal logic control of dynamical systems
• Robust discrete synthesis against unspecified disturbances
• Synthesis using approximately bisimilar abstractions, state-feedback controllers for safety specifications

Cites work

• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• Approximation Metrics for Discrete and Continuous Systems
• Augmented finite transition systems as abstractions for control synthesis
• Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications
• Feedback Refinement Relations for the Synthesis of Symbolic Controllers
• Finite abstractions with robustness margins for temporal logic-based control synthesis
• Formal methods for discrete-time dynamical systems
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 2209335 (Why is no real title available?)
• Some tractable supervisory control problems for discrete-event systems modeled by Buchi automata
• Symbolic Control of Linear Systems Based on Symbolic Subsystems
• Symbolic Models for Nonlinear Control Systems Without Stability Assumptions
• Symbolic models for nonlinear control systems: alternating approximate bisimulations
• Three Partition Refinement Algorithms
• Verification and Control of Hybrid Systems

This page was built for publication: Robust stutter bisimulation for abstraction and controller synthesis with disturbance

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