$\omega$-正则语言的四值可监控性

运行时验证(RV)是一种轻量级形式化技术，其中对程序或系统执行进行监控与分析，以在有限步数后检查某些性质是否被满足或违反。RV的使用引发了对判定性质是否可监控的兴趣：是否在有限的未来延续后总能确定该性质的满足或违反。然而，经典二值可监控性存在两个固有局限。首先，性质只能被评价为可监控或不可监控；关于是否仅能检测一种判定（满足或违反）毫无信息。其次，可监控性定义于语言层面，无法告知在系统执行期间从当前监控状态出发能否检测到满足或违反。为克服这些局限，本文提出$\omega$-语言的四值可监控性新概念，并将其应用于状态层面。四值可监控性比二值可监控性信息更丰富，因为性质可被评价为四值结果，表示对于可监控性质仅满足、仅违反或两者皆活跃。我们还可计算状态级弱可监控性，即从一个给定监控状态出发能否检测到满足或违反，从而实现监控算法的状态级优化。基于一种新的六值语义，我们提出了在语言层面与状态层面计算$\omega$-正则语言四值可监控性的过程。我们开发了一个新工具，实现了所提的LTL公式可监控性计算过程。