Formal Verification in a First-Order Extension of Modal μ-calculus
-
- OKAMOTO Keishi
- Research Center for Verification and Semantics, National Institute of Advanced Industrial Science and Technology (AIST)
Bibliographic Information
- Other Title
-
- 命題様相μ計算の一階拡張における形式的検証
Abstract
Formal verification is frequently based on modal μ-calculus and its fragments. However, the number of systems and verification properties which cannot be formalized in modal μ-calculus has been increasing as they become complicated. In this paper, we present a first-order extension of modal μ-calculus in order to formalize various such systems and verification properties. We also give an axiomatization of the logic. It is necessarily incomplete for the logic because the set of all valid formulas is not recursively enumerable. Finally, in order to demonstrate that our axiomatization is practical for verification, we formalize a system and mutual exclusion for unboundedly many processes in our first-order extension, and then verify that the system satisfies the property in our axiomatization.
Journal
-
- Computer Software
-
Computer Software 26 (1), 103-110, 2009
Japan Society for Software Science and Technology
- Tweet
Details 詳細情報について
-
- CRID
- 1390001204736478720
-
- NII Article ID
- 130004549126
-
- ISSN
- 02896540
-
- Data Source
-
- JaLC
- CiNii Articles
-
- Abstract License Flag
- Disallowed