Logical foundations of hierarchical model checking
Data Technologies and Applications
ISSN: 2514-9288
Article publication date: 29 August 2018
Issue publication date: 4 October 2018
Abstract
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.
Keywords
Acknowledgements
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).
Citation
Kamide, N. (2018), "Logical foundations of hierarchical model checking", Data Technologies and Applications, Vol. 52 No. 4, pp. 539-563. https://doi.org/10.1108/DTA-01-2018-0002
Publisher
:Emerald Publishing Limited
Copyright © 2018, Emerald Publishing Limited