Pre- and Post-Conditions Expressed in Variants of the Modal μ-Calculus

スポンサーリンク

概要

• 論文の詳細を見る

• 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.

• （社）電子情報通信学会の論文
• 2009-05-01

著者

• TAKAHASHI Koichi

  Research Center for Verification and Semantics (CVS), National Institute of Advanced Industrial Scie

• Tanabe Yoshinori

  Graduate School Of Information Science And Technology The University Of Tokyo

• Sekizawa Toshifusa

  Research Center For Verification And Semantics National Institute Of Advanced Industrial Science And

• YUASA Yoshifumi

  Graduate School of Information Science and Engineering, Tokyo Institute of Technology

• Yuasa Yoshifumi

  Graduate School Of Information Science And Engineering Tokyo Institute Of Technology

• Takahashi Koichi

  Research Center For Verification And Semantics National Institute Of Advanced Industrial Science And

• Takahashi Koichi

  Research Center For Verification And Semantics (cvs) National Institute Of Advanced Industrial Scien

関連論文

• Probabilistic Model Checking of the One-Dimensional Ising Model
• Probabilistic Model Checking of the One-Dimensional Ising Model
• Pre- and Post-Conditions Expressed in Variants of the Modal μ-Calculus
• Modal μ-calculus on Min-plus Algebra N∞

スポンサーリンク