Logics and translations for hierarchical model checking

被引：12

作者：

Kamide, Norihiro ^{[1
]}

Yano, Ryu ^{[2
]}

机构：

[1] Teikyo Univ, Fac Sci & Engn, Dept Informat & Elect Engn, Toyosatodai 1-1, Utsunomiya, Tochigi 3208551, Japan

[2] Teikyo Univ, Fac Sci & Engn, Dept Human Informat Syst, Toyosatodai 1-1, Utsunomiya, Tochigi 3208551, Japan

来源：

KNOWLEDGE-BASED AND INTELLIGENT INFORMATION & ENGINEERING SYSTEMS | 2017年 / 112卷

关键词：

Linear-time temporal logic; Computation tree logic; Hierarchical model checking; Sequence modal operator; COMPUTATION-TREE LOGIC;

D O I：

10.1016/j.procs.2017.08.014

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL) and computation-tree logic (CTL). Hierarchical model checking is a model checking paradigm that can appropriately verify systems with hierarchical information and structures. A sequential linear-time temporal logic (sLTL) and a sequential computation-tree logic (sCTL), which can suitably represent hierarchical information and structures, are developed by extending LTL and CTL, respectively. Translations from sLTL and sCTL into LTL and CTL, respectively, are defined, and theorems for embedding sLTL and sCTL into LTL and CTL, respectively, are proved using these translations. These embedding theorems allow us to reuse the standard LTL- and CTL-based model checking algorithms to verify hierarchical systems that are modeled and specified by sLTL and sCTL. (C) 2017 The Authors. Published by Elsevier B.V.

引用

页码：31 / 40

页数：10

共 50 条

[1] Foundations of Inconsistency-Tolerant Model Checking: Logics, Translations, and Examples
Kamide, Norihiro
Endo, Kazuki
[J]. AGENTS AND ARTIFICIAL INTELLIGENCE, ICAART 2018, 2019, 11352 : 312 - 342
[2] Interval temporal logics model checking
Montanari, Angelo
[J]. PROCEEDINGS 23RD INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING - TIME 2016, 2016, : 2 - 2
[3] Symbolic model checking of logics with actions
Pecheur, Charles
Raimondi, Franco
[J]. MODEL CHECKING AND ARTIFICIAL INTELLIGENCE, 2007, 4428 : 113 - +
[4] Model checking branching time logics
Schnoebelen, Ph.
[J]. TIME 2007: 14th International Symposium on Temporal Representation and Reasoning, Proceedings, 2007, : 5 - 5
[5] Tableaux and Model Checking for Memory Logics
Areces, Carlos
Figueira, Diego
Gorin, Daniel
Mera, Sergio
[J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, PROCEEDINGS, 2009, 5607 : 47 - +
[6] The complexity of model checking for propositional default logics
Liberatore, P
Schaerf, M
[J]. ECAI 1998: 13TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 1998, : 18 - 22
[7] Model checking games for branching time logics
Lange, Martin
Stirling, Colin
[J]. Journal of Logic and Computation, 2002, 12 (04) : 623 - 639
[8] Integrating temporal logics and model checking algorithms
Rus, T
Van Wyk, E
[J]. TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, 1997, 1231 : 95 - 110
[9] Spatial logics and model checking for medical imaging
Buonamici, Fabrizio
Belmonte, Gina
Ciancia, Vincenzo
Latella, Diego
Massink, Mieke
[J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2020, 22 (02) : 195 - 217
[10] Model checking for extended timed temporal logics
Bouajjani, A
Lakhnech, Y
Yovine, S
[J]. FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1996, 1135 : 306 - 326

← 1 2 3 4 5 →