Pre- and Post-conditions Expressed in Variants of the Modal μ-calculus
by
Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi
IEICE Transactions on Information and Systems,
Vol.E92-D, No.5, May 2009 (to appear).
Abstract
Properties of Kripke structures can be expressed by formulas of
the modal μ-calculus. Despite its strong expressive power, the
validity problem of the modal μ-calculus is decidable, and so
are some of its variants enriched by inverse programs, graded
modalities, and nominals. In this study, we show that the pre- and
post-conditions of transformations of Kripke structures, such as
addition/deletion of states and edges, can be expressed using variants of
the modal μ-calculus.
Combined with decision procedures we have developed for
those variants, the properties of sequences of
transformations on Kripke structures can be deduced.
We show that these techniques can be used to verify the properties of
pointer-manipulating programs.
Previous versions
home