TY  - JOUR
AB  - Purpose The 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/approach In 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.Findings These 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/value The 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.
VL  - 52
IS  - 4
SN  - 2514-9288
DO  - 10.1108/DTA-01-2018-0002
UR  - https://doi.org/10.1108/DTA-01-2018-0002
AU  - Kamide Norihiro
PY  - 2018
Y1  - 2018/01/01
TI  - Logical foundations of hierarchical model checking
T2  - Data Technologies and Applications
PB  - Emerald Publishing Limited
SP  - 539
EP  - 563
Y2  - 2024/04/23
ER  -