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.
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.
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*.
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.
The author would like to thank the anonymous referees for their valuable comments. This research was supported by JSPS KAKENHI Grant Numbers JP18K11171, JP16KK0007 and JSPS Core-to-Core Program (A. Advanced Research Networks). This research has also been supported by the Kayamori Foundation of Informational Science Advancement. A preliminary short version of the results of this paper was published in the Proceedings of the 21st International Conference on Knowledge-Based and Intelligent Information and Engineering Systems (KES 2017) (Kamide and Yano, 2017).
CitationDownload as .RIS
Emerald Publishing Limited
Copyright © 2018, Emerald Publishing Limited