Chapter 4 Regular Properties （正则属性）
本章讨论了一些基本算法，以验证重要的安全性、活性和广泛的其他线性时间特性。我们首先考虑正则安全属性，即其坏前缀构成正则语言的安全属性，因此可以由有限自动机识别。对于给定的有限转移系统TS，检查安全属性Psafe的算法依赖于使用识别Psafe坏前缀的有限自动机对TS的特定乘积构造中的不变检查问题进行简化。
然后**，我们将这种基于自动机的验证算法推广到一类更大的线性时间属性，即所谓的ω-正则属性。这类属性包括常规安全属性，但也包括许多其他相关属性，如各种活性属性。ω-正则性质可以用所谓的Büchi自动机来表示，Büchi自动机是有限自动机的一种变体，它接受无限（而不是有限）单词。**Büchi自动机将是通过减少持久性检查来验证ω-正则性的关键概念。后者是不变检查的一种变体，旨在表明某个状态条件从某个时刻起持续保持。
4.1 Automata on Finite Words （有限字上的自动机）
Definition 4.1. Nondeterministic Finite Automaton (NFA)（不确定有限自动机）
Definition 4.9. Deterministic Finite Automaton (DFA) （确定有限自动机）
4.2 Model-Checking Regular Safety Properties(模型检查常规安全属性)
4.2.1 Regular Safety Properties
[绝好的文章]((1条消息) 写给学生看的系统分析与验证笔记（九）——验证正则安全性(verifying regular safety properties)_Campsisgrandiflora的博客-CSDN博客)
Example 4.13. Regular Safety Property for Mutual Exclusion Algorithms
Example 4.13. Regular Safety Property for Mutual Exclusion Algorithms
Example 4.14. Regular Safety Property for the Traffic Light
Example 4.15. A Nonregular Safety Property
4.2.2 Verifying Regular Safety Properties(验证正则安全属性)
##### Definition 4.16. Product of Transition System and NFA
Theorem 4.19. Verification of Regular Safety Properties
4.3 Automata on Infinite Words
4.3.1 ω-Regular Languages and Properties
Definition 4.23. ω-Regular Expression
Definition 4.24. ω-Regular Language
Definition 4.25. ω-Regular Properties
Example 4.26. Mutual Exclusion
4.3.2 Nondeterministic Büchi Automata
Definition 4.27. Nondeterministic Büchi Automaton (NBA)
Example 4.29. Infinitely Often Green
