Computation for Supremal Simulation-Based Controllable and Strong Observable Subautomata

TL;DR

This paper develops a lattice-theoretic framework and algorithms to compute the largest subautomata that satisfy simulation-based controllability and strong observability, addressing limitations of existing specifications.

Contribution

It introduces a novel approach using three monotone operators and inequalities to compute the supremal simulation-based controllable and strong observable subautomata.

Findings

Proposes a lattice-based method for subautomata computation.

Provides an algorithm to find the supremal subautomata.

Establishes conditions for the existence of the supremal solution.

Abstract

Bisimulation relation has been successfully applied to computer science and control theory. In our previous work, simulation-based controllability and simulation-based observability are proposed, under which the existence of bisimilarity supervisor is guaranteed. However, a given specification automaton may not satisfy these conditions, and a natural question is how to compute a maximum permissive subspecification. This paper aims to answer this question and investigate the computation of the supremal simulation-based controllable and strong observable subautomata with respect to given specifications by the lattice theory. In order to achieve the supremal solution, three monotone operators, namely simulation operator, controllable operator and strong observable operator, are proposed upon the established complete lattice. Then, inequalities based on these operators are formulated, whose solution is the simulation-based controllable and strong observable set. In particular, a sufficient condition is presented to guarantee the existence of the supremal simulation-based controllable and strong observable subautomata. Furthermore, an algorithm is proposed to compute such subautomata.