《Principles of Model Checking》Chapter 4 Regular Properties

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

4.3.3 Deterministic Büchi Automata

4.4 Model-Checking ω-Regular Properties