Logical foundations of hierarchical model checking
Logical foundations of hierarchical model checking
复制标题
层次模型检验的逻辑基础
DOI：
10.1108/dta-01-2018-0002
复制
发表时间：
2018
影响因子：
1.6
通讯作者：
Norihiro Kamide
中科院分区：
文献类型：
--
作者：
Shun Kimura;Koujin Takeda;Norihiro Kamide
目的本文的目的是为分层模型检查开发新的简单逻辑和翻译。分层模型检查是一种模型检查范式，可以适当地验证具有分层信息和结构的系统。设计/方法/途径在本研究中，分层模型检查的逻辑和翻译是基于线性时间时序逻辑（LTL）、计算树逻辑（CTL）和全计算树逻辑（CTL*）开发的。通过扩展LTL、CTL和CTL*，分别开发了能够适当表示层次信息和结构的顺序线性时间时序逻辑（sLTL）、顺序计算树逻辑（sCTL）和顺序全计算树逻辑（sCTL*）。定义了从 sLTL、sCTL 和 sCTL* 分别到 LTL、CTL 和 CTL* 的翻译，并且使用这些翻译证明了将 sLTL、sCTL 和 sCTL* 分别嵌入到 LTL、CTL 和 CTL* 的定理。发现这些嵌入定理允许我们重用基于标准 LTL、CTL 和 CTL* 的模型检查算法来验证层次结构原创性/价值开发了新的逻辑sLTL、sCTL和sCTL*及其翻译，并基于这些逻辑和翻译提出了分层模型检查的一些说明性示例。
PurposeThe purpose of this paper is to develop new simple logics and translations for hierarchical model checking. Hierarchical model checking is a model-checking paradigm that can appropriately verify systems with hierarchical information and structures.Design/methodology/approachIn this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL), computation-tree logic (CTL) and full computation-tree logic (CTL*). A sequential linear-time temporal logic (sLTL), a sequential computation-tree logic (sCTL), and a sequential full computation-tree logic (sCTL*), which can suitably represent hierarchical information and structures, are developed by extending LTL, CTL and CTL*, respectively. Translations from sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are defined, and theorems for embedding sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are proved using these translations.FindingsThese embedding theorems allow us to reuse the standard LTL-, CTL-, and CTL*-based model-checking algorithms to verify hierarchical systems that are modeled and specified by sLTL, sCTL and sCTL*.Originality/valueThe new logics sLTL, sCTL and sCTL* and their translations are developed, and some illustrative examples of hierarchical model checking are presented based on these logics and translations.
登录
查看更多内容
使用序列模态运算符扩展完整计算树逻辑：表示分层树结构
DOI：
10.1007/978-3-642-10439-8_49
发表时间：
2009
期刊：
--
影响因子：
--
作者：
N. Kamide;K. Kaneiwa
通讯作者：
K. Kaneiwa
DOI：
--
发表时间：
1993
期刊：
Lecture Notes in Computer Science
影响因子：
--
作者：
H. Wansing
通讯作者：
H. Wansing
分布式并发线性逻辑编程
DOI：
10.1016/s0304-3975(99)00052-3
发表时间：
1999
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
N. Kobayashi;Toshihiro Shimizu;A. Yonezawa
通讯作者：
A. Yonezawa
序列索引线性时间时态逻辑：证明系统和应用
影响因子：
2.8
作者：
K. Kaneiwa;N. Kamide
通讯作者：
N. Kamide