Logics and translations for hierarchical model checking

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.