前言

经过这么多知识的准备，终于可以开始验证ω-正则属性了，之前介绍的ω-正则属性和NBA的知识都会用上

首先回顾一下我们是怎么做正则安全性的验证的，如下图所示

现在我们要验证的是ω-正则属性，其实总体流程都是一样的，先要有一个TS模型，然后将属性转换为接受坏行为的自动机，现在我们要用的自动机是NBA，并用P‾\overline{P}P表示坏行为，用相同的运算⊗\otimes⊗构建新TS，最后验证的F条件也发生了变化，我们也会介绍新的算法。

如果忘了啥叫ω-正则属性和NBA，看看这篇Büchi自动机

好，介绍结束，现在开始回归问题

给定一个TS和一个ω-正则属性P，如何判断TS⊨PTS\vDash PTS⊨P?

建立对应系统坏行为的NBA,记为A，例如，Lω(A)=(2AP)ω∖PL_{ω}(A)=(2^{AP})^ω\setminus PLω(A)=(2AP)ω∖P
检查Traces(TS)∩Lω(A)=∅Traces(TS)\cap L_{ω}(A)=\varnothingTraces(TS)∩Lω(A)=∅是否成立（就是检查TS系统里面是否存在不满足属性的坏行为）
为了做到上面的检查，需要利用运算TS⊗ATS\otimes ATS⊗A生成新的TS，并检查TS⊗ATS\otimes ATS⊗A满足永远不会形成接受A的情况

对于这里的第三步，对一个NBA来说，接受的情况是指可以使得NBA无限经常次访问F，不能满足接受，可以用语言表示为有限经常次访问F，我们需要用到TS上持续性(persistence property)的知识。

持续性

设PpersP_{pers}Ppers为LT属性，并且Ppers⊆(2AP)ωP_{pers}\subseteq (2^{AP})^ωPpers⊆(2AP)ω，P如果被称为持续性，那么存在AP上的命题逻辑公式ϕ\phiϕ，使得
Ppers={A0A1A2...∈(2AP)ω∣∃i≥0.∀j≥i.Aj⊨ϕ}P_{pers}=\{A_{0}A_{1}A_{2}...∈(2^{AP})^ω|\exist i≥0.\forall j≥i.A_{j}\vDash\phi\} Ppers={A0A1A2...∈(2AP)ω∣∃i≥0.∀j≥i.Aj⊨ϕ}

就是说当某个时间点之后，ϕ\phiϕ将会一直成立（用后面章节的LTL表示就是◊□ϕ\Diamond\Box\phi◊□ϕ）

这里的ϕ\phiϕ被称为PpersP_{pers}Ppers的持续条件

看到上面图片的"TS⊗A⊨有限经常次访问FTS\otimes A\vDash有限经常次访问FTS⊗A⊨有限经常次访问F"，“有限经常次访问F”表示在前面的某一段时间内可以访问F，但是当到达某一个时间点之后，就再也不会访问F，如果使用持续性的表达方式，这句话也可以换一种表达方式为"eventuallyforever¬Feventually\text{ }forever\text{ }\lnot Feventually forever ¬F"，这句话的持续条件就是¬F\lnot F¬F

验证ω-正则属性

给定不存在终止状态的TS=(S,Act,→,I,AP,L)TS=(S, Act, →,I,AP, L)TS=(S,Act,→,I,AP,L)，以及一个非阻塞的NBAA=(Q,Σ,δ,Q0,F)A = (Q, Σ, δ, Q_{0}, F)A=(Q,Σ,δ,Q0,F)，非阻塞(non-blocking)的意思是，对于NBA的每个状态来说，接受任意输入都能转换为下一个状态，而不会受到阻塞。这个NBA用来表示ω-正则属性P的坏行为。

生成新的TS过程与验证正则安全性几乎是一样的，因为NBA和NFA的表示方式相同，运算过程和⊗\otimes⊗符号详细请看验证正则安全性

对于ω-正则属性的模型检测，下面几种陈述都是等价的

T⊨PT\vDash PT⊨P
Traces(TS)∩Lω(A)=∅Traces(TS)\cap L_{ω}(A)=\varnothingTraces(TS)∩Lω(A)=∅
TS⊗A⊨eventuallyforever¬FTS\otimes A\vDash eventually\text{ }forever\text{ }\lnot FTS⊗A⊨eventually forever ¬F

举例

现在我们有一个简单的红绿灯TS系统

嗯，实在是够简单的，毕竟是用作例子嘛

现在它有一个属性P“无限经常次会出现绿灯”（咳咳，我知道稍微瞄一眼就知道这个是对的，但是现在我们假装不知道这个属性是否成立）

为了验证这个性质是否成立，我们需要构建一个接受坏行为的NBA

对于这个属性坏行为就是取P的补，是指“有限经常次出现green”或者“最终永远不会出现green”

所以我们为这个坏行为构建了一个NBA，解释一下，首先在q0q_{0}q0上的true表示了一个有限的片段，在这个有限的片段里面，出现什么都无所谓，然后到了某一个时间点，也就是q0q_{0}q0到q1q_{1}q1的这个转换，输入的¬green\lnot green¬green代表了这个时间点，在这个时间点之后，就再也不会出现green了，将会一直出现¬green\lnot green¬green循环，因为一旦在这个时间点后出现了green，那么NBA就会转换到q2q_{2}q2，导致无法无限经常次访问q1q_{1}q1，该输入也就不能被NBA接受

有了TS模型和坏行为代表的NBA，接下来就该构建新的TS了，利用⊗\otimes⊗计算，得出

我们要检查的是eventuallyforever¬Feventually\text{ }forever\text{ }\lnot Feventually forever ¬F，看看它最终会不会永远不访问qFq_{F}qF呢？这里的接受状态qFq_{F}qF指的是q1q_{1}q1，让我们来看一下，虽然它会经过q1q_{1}q1，但也就最多经过一次，之后就再也不会经过了，所以是能够满足最终永远¬F\lnot F¬F这个条件的，即该TS能够满足属性P

既然讲完了模型检测的方法，又到了最后讲算法的环节啦，我们如何用一种算法表示上述检查eventuallyforever¬Feventually\text{ }forever\text{ }\lnot Feventually forever ¬F的步骤？简单来说就是在新的TS上找环，看看一个可达状态qFq_{F}qF是否在图中的一个环里面，如果它在环里面，那么说明它可能无限经常次被访问，即TS⊭PTS\nvDash PTS⊭P，如果不在环里就说明TS⊨PTS\vDash PTS⊨P，看看上面的图，状态q1q_{1}q1并不在任何一个环里面。

接下来把红绿灯的模型换一换

最终生成的TS系统成为了这个样子，此时状态q1q_{1}q1在一个环里面，所以这个系统不满足“无限经常次会出现绿灯”这一性质

算法的话就是图上的强连通分量（SCC）的问题，求解SCC需要基于所有的可达状态，除了基于强连通分量的方法外还有一种基于nested DFS的算法，该算法在最坏情况下仍要遍历所有的节点，但是也有可能提前终止，代码贴在Nested Dfs算法

写给学生看的系统分析与验证笔记（十二）——验证ω-正则属性(Verifying ω-regular properties)相关推荐

写给学生看的系统分析与验证笔记（七）——线性时间属性（Linear-Time Properties）
目录路径和状态图(Paths and State Graph) 状态图路径迹(trace) 刻画线性时间属性(LT Properties) 刻画基于信号量互斥系统的属性刻画无饥饿(starva ...
写给学生看的系统分析与验证笔记（九）——验证正则安全性(verifying regular safety properties)
目录正则安全性验证正则安全性总结之前我们将系统建模为了抽象的模型,并且刻画了相应的性质,现在终于到了模型检测最后一步--验证(verification) 如果我们将真实的系统建模为了TS,并且 ...
写给学生看的系统分析与验证笔记（十五）——计算树逻辑(Computation tree logic,CTL)
目录介绍计算树线性时间和分支时间的对比 CTL的语法 CTL的语义 CTL状态公式的语义 CTL路径公式的语义 CTL在TS上的语义 CTL等价的定义 CTL公式的性质介绍在前面我们已经介绍 ...
《The Non-Designer's Design Book(写给大家看的设计书)》--笔记整理
The Non-Designer's Design Book(写给大家看的设计书)-笔记整理这是一本实用性书籍,阐述了设计中的四大原则:亲密性.对齐.重复和对比,并介绍了如何运用颜色.字体,以及针对 ...
【大厂面试】面试官看了赞不绝口的Redis笔记（二）
文章目录说明四.Redis的其他功能 (一)慢查询 (二)pipeline (三)发布订阅 (四)Bitmap (五)HyperLogLog (六)GEO 五.Redis持久化的取舍和选择 (一) ...
写给大家看的设计书阅读笔记1——设计的四大基本原则
设计的四大基本原则概述有一些基本的设计原则,每一个优秀的设计中都应用了这些原则.我们在观察评价一个设计作品时,也要从这几条基本原则去考虑. 亲密性 Proximity 彼此相关的项应当靠近,归组在一 ...
以前看书时记得一些笔记（二），很早了，现在再看都有些看不懂了
MFC学习: 1.CObject类为MFC总类,该类下面有一个重要的类CCmdTarget.而CCmdTarget类下面又有四个重要的继承类,分别为:CWinThread.CDocument.CDoc ...
《写给大家看的设计书》《写给大家看的色彩书》《点石成金》《形式感》学习笔记...
为什么80%的码农都做不了架构师?>>> 首发:个人博客,更新&纠错&回复今天读了四本书<写给大家看的设计书><写给大家看的色彩书>& ...
《写给大家看的设计书》《写给大家看的色彩书》《点石成金》《形式感》学习笔记
首发:个人博客,更新&纠错&回复今天读了四本书<写给大家看的设计书><写给大家看的色彩书><点石成金>和<形式感>,学习学习设计. 笔 ...
【大厂面试】面试官看了赞不绝口的Redis笔记
文章目录一.Redis简介二.Redis API的使用和理解 (一)通用命令 (二)单线程架构 (三)数据结构和内部编码 (四)字符串 (五)hash (字典) (六)列表 (七)Set集合 (八 ...

写给学生看的系统分析与验证笔记（十二）——验证ω-正则属性(Verifying ω-regular properties)

目录

前言

持续性

验证ω-正则属性

写给学生看的系统分析与验证笔记（十二）——验证ω-正则属性(Verifying ω-regular properties)相关推荐

最新文章

热门文章