基于模拟的可控与强可观测最大子自动机的计算
Computation for Supremal Simulation-Based Controllable and Strong Observable Subautomata
AI总结：
针对给定规范自动机不满足模拟可控性和模拟可观测性的情况，利用格理论提出三个单调算子，通过求解不等式得到最大模拟可控且强可观测的子自动机，并给出存在性条件和算法。
摘要：
双模拟关系已成功应用于计算机科学和控制理论。在我们先前的工作中，提出了基于模拟的可控性和基于模拟的可观测性，在这些条件下保证了双模拟监督器的存在性。然而，给定的规范自动机可能不满足这些条件，一个自然的问题是如何计算最大允许的子规范。本文旨在回答这个问题，并利用格理论研究相对于给定规范的最大模拟可控且强可观测子自动机的计算。为了获得最大解，在建立的完备格上提出了三个单调算子，即模拟算子、可控算子和强可观测算子。然后，基于这些算子建立了不等式，其解即为基于模拟的可控且强可观测集。特别地，给出了一个充分条件以保证最大模拟可控且强可观测子自动机的存在性。此外，提出了一种算法来计算这样的子自动机。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
