-
《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
-
相关阅读:
php利用ZipArchive类实现文件压缩与解压
防御塔攻击小兵，C++观察者模式
2024年山东省职业院校技能大赛中职组 “网络安全”赛项竞赛试题-C卷
const的自己理解
SAP ABAP OData 服务如何支持 $select 有选择性地仅读取部分模型字段值试读版
阿里云服务器ECS共享型和企业级是什么？
SFI立昌STN方案与应用
打怪升级（考验思路）
基于遗传算法解决的多仓库多旅行推销员问题（Matlab代码实现）
springboot中使用poi导出excel文件，下载简易模板（根据对象实体类生成表头）
- 原文地址：https://blog.csdn.net/qq_40893490/article/details/126909124