admin管理员组文章数量:1530018
目录
1. 引言
2. LTL
2.1 Action的逻辑
3. FSP—流动性
3.1 FSP– Indexed fluents
4. FSP – Fluent expressions
5. 时间逻辑—“always” 和 “eventually”
5.1 时间逻辑—“always”
5.2 时间逻辑—“eventually”
6. FSP – Safety and liveness
7. 结合时间性运算符
8. 时间逻辑法则
9. 时间逻辑的表达能力
10. 时间逻辑—“until”操作符
11. 时间逻辑—“next”操作符
12. 重新审视相互排斥
13. 表达Mutex的安全性和活泼性
14. 现实世界中的模型检查
1. 引言
在上两讲中，我们看到如何指定对并发系统的每一次执行都成立的属性。这些安全和有效性属性对于描述系统的某些属性非常有用。然而，它们并不像逻辑属性那样强大。
逻辑属性是由命题和逻辑运算符组成的描述，如and、not和or。你可能已经学过命题逻辑，它允许我们描述关于系统在某一瞬间的状态的属性。然而，FSP模型没有状态，它的时间是线性的，连续的，它们由在连续时间中发生的动作组成。
2. LTL
我们如何解决上述问题，为FSP模型添加命题逻辑。在这里，我们超越了命题逻辑和安全/有效性属性，而采用了线性时态逻辑（LTL）。
LTL谓词给了我们比命题逻辑或安全/有效性属性更大的灵活性，并允许我们指定更复杂的系统属性，然后可以用LTSA进行检查。
2.1 Action的逻辑
逻辑学中的原子命题涉及到系统的状态。在软件分析中，这通常是基本命题，如和。我们该如何思考并发模型的逻辑呢？首先我们提供一个思路：
因为在并发的模型中，我们通常关注的是action，以及它们发生的顺序。我们可以采用命题逻辑的思想，说当action a执行时，命题a是真的，而在执行其他action的时候命题a是假的。但这种思路有问题，因为每次只有一个命题是真的。
实际上，我们感兴趣的是关于一段时间内的行动序列的属性，而不仅仅是一个瞬间的时间。时间逻辑允许我们谈论持续时间和事件的相对时间（相对于绝对时间）。
3. FSP—流动性
fluent是一种可以随时间变化的属性。
fluent使我们能够描述一个系统在其生命周期中的属性，而不仅仅是在一个瞬间。
fluent被大量用于逻辑学，特别是人工智能。
在FSP中，一个fluent被描述为：
fluent FL = <{s1,...,sN}, {e1,...,eN}>和都是actions：
fluent FLfluent FL是一个命题，当中的任何一个动作发生时，FL变成了True。而当中的任何一个动作发生时，FL又变为False。
如果我们想要一个最初是True的fluent，我们可以用以下方式来描述它：
fluent FL = <{s1,...,sN}, {e1,...,eN}> initially 11 代表 true，0 代表 false
以交通灯系统为例，当我们预计绿灯亮的时候，我们可以说：
fluent GREEN = <{green}, {yellow ,red}> initially 1也就是说，当绿色动作发生时，fluent GREEN为真，而当黄色或红色发生时，fluent 为假。
因此，这个 fluent 不是一个动作：当黄色或红色以外的动作发生时（比如说，动作 wander 或者 none），它仍然是真的，尽管动作绿色目前不是真的。
3.1 FSP– Indexed fluents
与进程一样，我们可以为两个灯定义索引 fluents：
fluent GREEN[i:1..2]
= <{green[i]}, {yellow[i],red[i]}> initially 14. FSP – Fluent expressions
Fluents 可以使用命题逻辑连接词进行组合。
此外，我们还有（有界的）普遍性和存在性量词：
forall[i:1..2] GREEN[i]
exists[i:1..2] GREEN[i]现在我们可以表示，我们不希望两个灯同时是绿色的&#
版权声明：本文标题：FSP语言学习（十）：用时态逻辑进行模型检查 内容由热心网友自发贡献，该文观点仅代表作者本人， 转载请联系作者并注明出处：https://m.elefans.com/dianzi/1726654226a1080064.html， 本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌抄袭侵权/违法违规的内容，一经查实，本站将立刻删除。
发表评论