- 博客(3)
- 收藏
- 关注
RSS订阅原创 模型检测学习笔记（一）：绪论
一、概念 模型检测是一种用于自动验证有限状态并发系统的技术；模型检测算法通常对系统状态空间进行穷尽搜索来确定性质的真假。如果资源充足，检测过程总是以是或非终止，是表示系统满足性质，否表示不满足性质，并自动给出一个反例。模型检测中最大的困难是状态空间爆炸；解决状态空间爆炸有如下方法：符号化模型检验技术； 偏序规约技术； on-the-fly技术； 对称技术； 抽象和组合技术；二...
2018-10-15 19:09:54
4938
原创 Petri网学习（五）：Petri网子类的性质分析
一、标识S-图S-图定义：定义：网N=(P,T;F)是S-图或状态机当且仅当：，而带有标识的S-图称为标识S-图。将S-图中的变迁撤掉可以简化为有向图SG=(P,E)我对S-图的理解：所有的变迁都是单进单出。S-图的性质：1、设N=(P,E)是一个S-图，则；（运行过程中标识数不变）2、若N是一个S-图，对于任意的初始标识M0，（N,M0）都是有界的；3、...
2018-10-14 21:12:02
2585
1
原创 Petri网学习（四）：Petri网的结构性质
一、结构有界性&守恒性1. 结构有界性定义：设N=(P,T;F)为一个网。对N赋予任意的初始标识M0，网(N,M0)都是有界的，则称N为结构有界网；再回忆一下什么是有界petri网：在PN=(P,T;F,M0)中，，库所p都有界，则称PN为有界petri网。区别在于是不是任意初始标识 什么是库所有界： 定理：设A为网N=(P,T;F)的关联矩阵，N是结构有界网的充分必...
2018-10-13 14:57:30
8155
1
空空如也
空空如也
TA创建的收藏夹 TA关注的收藏夹
TA关注的人