闵应骅的博客分享 http://blog.sciencenet.cn/u/ymin 一位IEEE终身Fellow对信息科学及其发展的看法

博文

模型检验(3)(091231)

已有 4741 次阅读 2009-12-31 11:36 |个人分类:学术导航|系统分类:科研笔记| 模型检验, 模型检验

模型检验(3)(091231)
闵应骅
    时态逻辑用来描述正确的系统行为,模型检验提供实用的硬件和软件验证方法。模型验证可形式地描述如下:给定一个有限结构M,状态s,和一个时态逻辑公式,问M, s |= f ?即问:在结构M中,于状态s0,f是否为真?或者说,给定M和f,计算这个集合{s : M, s |= f}。他们证明了这个问题的计算复杂性对公式和结构的大小是线性的。该算法是基于基本时态模型化的不动点原理。例如,如果f(Z)表示p ∨ AXZ。AFp = f (AFp)是f(Z)的不动点。因为AFp为真,当且仅当p为真,或者AXAFp为真。(意即以后p总会为真,当且仅当p现在就真,或者以后总会为真。)一般来说,可能有许多不动点,但这个是最小不动点,记为µZ = f (Z)。我们可以迭代地计算使得AFp为真的状态集。因为每一个公式都有一个使之为真的状态集。可以证明,单调递增序列false ⊆
f ( false) ⊆ f 2(false) ⊆ . . . ⊆ f k( false) = f k+1(false)揭示最小不动点,如果f(Z)是单调的。CTL模型验证是多项式复杂的,但LTL则是指数复杂的,不过可以接受。
    问题是时态逻辑公式的可表达性。就是说,什么样的特性可以用时态逻辑公式来表达?例如安全性(“无坏事发生”即G-bad),活性(“有些好事发生”,即Fgoal),及公平性(“有些事常发生”即GFtry)。我们需要用表达式表达所有正确性。如果这一点做不到,就无法使用模型检验。但实际上,时态逻辑公式能够做到这一点,而且接近自然语言。正因为这一点,我们需要LTL,CTL,和CTL*。
    另一个问题是简洁性,即表达是否简洁。例如CTL*公式E(Fp1 ∧ Fp2)不是一个CTL公式,但它等价于EF(p1 ∧ EFp2) ∨EF(p2 ∧ EFp1),这是一个CTL公式,虽然它比较长一些。
    另一个重要问题是有效性,即对于电路或逻辑,模型验证问题的复杂性及模型验证算法的性能。当然,可表达性、简洁性和有效性是有矛盾的,需要某些折中。一般要求M少于1,000,000个状态。对于状态特别多的机器,可以设法省略一些非本质的详情,以简化M。有人也提出用所谓符号模型检验来处理复杂的机器。这方面的研究还很多,有人甚至考虑无限状态系统。

https://wap.sciencenet.cn/blog-290937-282881.html

上一篇:模型检验(2)(091231)
下一篇:模型检验(4)(091231)
收藏 IP: .*| 热度|

2 俞立 杨秀海

发表评论 评论 (0 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-3-29 05:14

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部