Robust Stutter Bisimulation for Abstraction and Controller Synthesis with Disturbance: Proofs

TL;DR

This paper introduces a robust stutter bisimulation method for creating finite abstractions of disturbed cyber-physical systems, enabling controller synthesis that guarantees LTL specifications despite uncertainties.

Contribution

It presents a novel robust stutter bisimulation relation and an algorithm to construct quotient systems, facilitating controller synthesis for systems with disturbances.

Findings

Algorithm successfully constructs robust bisimulation quotients

Controller existence is equivalent between original and abstract systems

Application demonstrated on robot navigation example

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.