Generation of Minimum Tree-Like Witnesses for Existential CTL
Generation of Minimum Tree-Like Witnesses for Existential CTL
复制标题
存在 CTL 的最小树状见证的生成
DOI：
10.1007/978-3-319-89960-2_18
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Ciardo, Gianfranco
中科院分区：
文献类型：
--
作者：
Jiang, Chuan;Ciardo, Gianfranco
模型检查的一个优点是它能够生成证明或反例。方法存在简单的非嵌套公式生成小或最小的证人，但没有现有的方法保证一般嵌套的最小。在这里，我们给出了一个定义的证人的大小，使用边值决策图递归计算每个子公式的最小证人的大小，并描述了一个一般的方法来建立最小的树形证人存在CTL。实验结果表明，对于某些模型，我们的方法是能够产生最少的证人，而传统的方法是不是。
An advantage of model checking is its ability to generate witnesses or counterexamples. Approaches exist to generate small or minimum witnesses for simple unnested formulas, but no existing method guarantees minimality for general nested ones. Here, we give a definition of witness size, use edge-valued decision diagrams to recursively compute the minimum witness size for each subformula, and describe a general approach to build minimum tree-like witnesses for existential CTL. Experimental results show that for some models, our approach is able to generate minimum witnesses while the traditional approach is not.
登录
查看更多内容
DOI：
10.1145/1029894.1029922
发表时间：
2004-10
期刊：
--
影响因子：
--
作者：
Jianbin Tan;G. Avrunin;L. Clarke;S. Zilberstein;S. Leue
通讯作者：
Jianbin Tan;G. Avrunin;L. Clarke;S. Zilberstein;S. Leue
使用“关键事件”制作简短的反例
影响因子：
0.8
作者：
Sujatha Kashyap;V. Garg
通讯作者：
V. Garg
最短EG见证生成的符号算法
DOI：
--
发表时间：
2011
期刊：
2011 Fifth International Conference on Theoretical Aspects of Software Engineering
影响因子：
--
作者：
Yang Zhao;Xiaoqing Jin;Gianfranco Ciardo
通讯作者：
Gianfranco Ciardo
DOI：
--
发表时间：
2010
期刊：
NASA Formal Methods
影响因子：
--
作者：
Yang Zhao;Gianfranco Ciardo
通讯作者：
Gianfranco Ciardo
使用 S m A r T 进行逻辑和随机建模
DOI：
--
发表时间：
2006
期刊：
Performance evaluation (Print)
影响因子：
--
作者：
Gianfranco Ciardo;R. L. Jones;Andrew S. Miner;Radu I. Siminiceanu
通讯作者：
Radu I. Siminiceanu