Logical foundations of hierarchical model checking

DOIhttps://doi.org/10.1108/DTA-01-2018-0002
Date04 September 2018
Publication Date04 September 2018
Pages539-563
AuthorNorihiro Kamide
SubjectLibrary & information science,Librarianship/library management,Library technology,Information behaviour & retrieval,Metadata,Information & knowledge management,Information & communications technology,Internet
Logical foundations of
hierarchical model checking
Norihiro Kamide
Department of Information and Electronic Engineering, Teikyo University,
Utsunomiya, Japan
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 tra nslations for hierarchical model ch ecking
are developed based on linear-time tempora l logic (LTL), comp utation-tree logic (CTL) and full
computation-tree log ic (CTL*). A sequential l inear-time temporal lo gic (sLTL), a sequentia l computation-
tree logic (sCTL), and a seq uential full computatio n-tree logic (sCTL*), w hich can suitably repre sent
hierarchical informa tion and structures, are developed by extending L TL, CTL and CTL*, respecti vely.
Translations from sLT L, sCTL and sCTL* into LTL, CT L and CTL*, respective ly, are defined, and
theorems for embeddin g 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 Translation, Computation-tree logic, Embedding theorem, Full computation-tree logic,
Hierarchical model checking, Linear-time temporal logic
Paper type Research paper
1. Introduction
The main aim of this s tudy is to develop n ew simple logics and translations for
hierarchical model checking, which is a new model-checking paradigm that can
appropriately ve rify systems with hierarchical information and structures. Model
checking is a formal method for verifying concurrent systems (Clarke and Emerson, 1981;
Clarke et al., 1999, 2018; Holzmann, 2006). A model of the system being considered is
expressed as temporal logic semantics, and system specifications are expressed as
temporal logic formulas. Efficient model-checking algorithms are used to determine
whether the specifications hold for the model.
Linear-time temporal logic (LTL) (Pnueli, 1977) is one of the most useful temporal logics
for model checking. LTL is based on the linear-time paradigm, which uses a linear order to
represent the passage of time. The model checker known as SPIN (Holzmann, 2006)
was developed based on LTL. Computation-tree logic (CTL) (Clarke and Emerson, 1981) is
also one of the most useful temporal logics for model checking. CTL is based on the
branching-time paradigm, which uses computation trees to represent the passage of time.
The model checker known as NuSMV (Cavada et al., 2015) was developed based
on both LTL and CTL. Full computation-tree logic (CTL*) (Clarke and Emerson, 1981;
Clarke et al., 1999; Holzmann, 2006) integrates LTL and CTL, and is also known to
be an important base logic for model checking. Because CTL* is more expressive
than both LTL and CTL, its formulas can be described based on both the linear- and
branching-time paradigms.
Standard temporal logics LTL, CTL and CTL* are unsuitable for specifying and
verifying systems with hierarchical information and structures because they lack
constructors for naturally representing such information. A suitable modal operator called a
Data Technologies and
Applications
Vol. 52 No. 4, 2018
pp. 539-563
© Emerald PublishingLimited
2514-9288
DOI 10.1108/DTA-01-2018-0002
Received 4 January 2018
Revised 8 April 2018
8 July 2018
Accepted 9 July 2018
The current issue and full text archive of this journal is available on Emerald Insight at:
www.emeraldinsight.com/2514-9288.htm
539
Hierarchical
model
checking
sequence modal operator is useful for representing informative and highly complex
hierarchical information and structures. Some extended temporal logics that employ a
sequence modal operator have been proposed and studied to handle hierarchical
information and structures (Kamide and Kaneiwa, 2009; Kaneiwa and Kamide, 2010, 2011;
Kamide, 2015). A brief survey of such extended logics is addressed in the last section
of this paper.
In this study, simple new temporal logics called sequential linear-time temporal logic
(sLTL), sequential computation-tree logic (sCTL) and 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*.
Although the previously proposed logics CTLS* (Kamide and Kaneiwa, 2009; Kaneiwa
and Kamide, 2011), SLTL (Kaneiwa and Kamide, 2010) and SPCTL (Kamide, 2015) have
complex multiple sequence-index ed satisfaction relations F^
d, where ^
drepresents
sequences, the proposed logics sLTL, sCTL and sCTL* have a simple single satisfaction
relation F
that is highly compatible with the standard single satisfaction relations of LTL,
CTL and CTL*. By using these simple satisfaction relations, the theorems for embedding
sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, can be proved simply, and
the sequence modal operator can be formalized simply and handled uniformly. In addition to
these advantages, sLTL is more expressive than SLTL because SLTL has no until and
release temporal operators. However, sLTL does use these operators.
The usefulness and intuitive meanings of the sequence modal operator are explained as
follows. The sequence modal operator, which is denoted as [b], where bis a sequence, is
useful for representing the concepts of hierarchical information, hierarchical trees, orders
and ontologies. This is plausible because a sequence structure gives a monoid M,;,
with the following informational interpretation (Wansing, 1993): Mis a set of pieces of
ordered information (i.e. a set of sequences); is a binary operator (on M) that combines two
pieces of information (i.e. it is a concatenation operator on sequences); and is an empty
piece of information (i.e. an empty sequence). Then, a formula in the form [b
1
;b
2
;;b
n
]α
intuitively means that αis true based on a sequence b
1
;b
2
;;b
n
of ordered pieces
of information.Furthermore, a fo rmula in the form []α, which coincides with α,
intuitively means that αis true without any information (i.e. it is an eternal truth in the
sense of classical logic).
The remainder of this paper is organized as follows.
In Section 2, we discuss the linear-time case, which is based on LTL and sLTL. The new
formulation sLTL is introduced based on the single satisfaction relation F
. In addition, we
define a new translation function from sLTL into LTL, which is considered a simplification
of the translation functions used in Kamide and Kaneiwa (2009), Kaneiwa and Kamide (2010,
2011) and Kamide (2015). The theorem for embedding sLTL into LTL is proved using the
proposed translation function.
In Section 3, we review the branching-time case, which is based on CTL and sCTL.
Similar to the sLTL case, the new formulation sCTL is introduced based on the single
satisfaction relation. In addition, a translation function from sCTL into CTL is defined, and
the theorem for embedding sCTL into CTL is proved.
In Section 4, we discuss the linear- and branching-time mixed case (i.e. full branching-
time case), which is based on CTL* and sCTL*. Our discussion is given in a similar manner
as that of the linear- and branching-time cases.
540
DTA
52,4

To continue reading

Request your trial

VLEX uses login cookies to provide you with a better browsing experience. If you click on 'Accept' or continue browsing this site we consider that you accept our cookie policy. ACCEPT