Logical foundations of hierarchical model checking

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.