关于Büchi自动机和Büchi自动机的注记
A Note on Monitors and Büchi automata
摘要：
当需要针对未知或非常复杂的系统检查属性时，模型检查等经典探索技术不再适用。有时可以使用~monitor，它在运行时检查底层系统上的给定属性。属性$L$的监视器是一个确定性有限自动机$M_L$，它在每次有限执行后告知（1）执行的每个可能的扩展是否都在$L$中，或者（2）每个可能的扩展是否都在$L$的补数中，或者（1）和（2）都不成立。此外，$L$是可监视的意味着在将来的某个时刻监视器总是可能达到（1）或（2）。可监控属性的经典例子是安全性和协同安全性。另一方面，像“无穷多个$a$”这样的确定性活性属性是不可监视的。我们讨论了各种监视器结构，重点是确定性的欧米茄-正则语言。我们找到一个适当的子类的确定性欧米茄-正则语言，但也严格大于子类的语言是确定性和共确定性，并为这个子类存在一个规范的监视器，也接受语言本身。我们还解决了这个问题，以决定可监控性相比，决定活性。现有技术如下。给定一个Büchi自动机，它是PSPACE完备的，可以决定它是活的还是可监控的。给定一个LTL公式，决定活性变得EXPSPACE完全，但决定可监控性的复杂性仍然是开放的。
英文摘要：
When a property needs to be checked against an unknown or very complex system, classical exploration techniques like model-checking are not applicable anymore. Sometimes a~monitor can be used, that checks a given property on the underlying system at runtime. A monitor for a property $L$ is a deterministic finite automaton $M_L$ that after each finite execution tells whether (1) every possible extension of the execution is in $L$, or (2) every possible extension is in the complement of $L$, or neither (1) nor (2) holds. Moreover, $L$ being monitorable means that it is always possible that in some future the monitor reaches (1) or (2). Classical examples for monitorable properties are safety and cosafety properties. On the other hand, deterministic liveness properties like "infinitely many $a$'s" are not monitorable. We discuss various monitor constructions with a focus on deterministic omega-regular languages. We locate a proper subclass of of deterministic omega-regular languages but also strictly large than the subclass of languages which are deterministic and codeterministic, and for this subclass there exists a canonical monitor which also accepts the language itself. We also address the problem to decide monitorability in comparison with deciding liveness. The state of the art is as follows. Given a Büchi automaton, it is PSPACE-complete to decide liveness or monitorability. Given an LTL formula, deciding liveness becomes EXPSPACE-complete, but the complexity to decide monitorability remains open.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
