Multi-Valued Modal Fixed Point Logics for Model Checking

スポンサーリンク

概要

• 論文の詳細を見る

• In this paper, I will show how multi-valued logics are used for model checking. Model checking is an automatic technique to analyze correctness of hardware and software systems. A model checker is based on a temporal logic or a modal fixed point logic. That is to say, a system to be checked is formalized as a Kripke model, a property to be satisfied by the system is formalized as a temporal formula or a modal formula, and the model checker checks that the Kripke model satisfies the formula. Although most existing model checkers are based on 2-valued logics, recently new attempts have been made to extend the underlying logics of model checkers to multi-valued logics. I will summarize these new results.

• 2010-08-01

著者

• NISHIZAWA Koki

  Department of Information Systems, Faculty of Environmental and Information Studies, Tottori Univers

• NISHIZAWA Koki

  Department of Information Systems, Faculty of Environmental and Information Studies, Tottori University of Environmental Studies

関連論文

• Multi-Valued Modal Fixed Point Logics for Model Checking
• Multi-Valued Modal Fixed Point Logics for Model Checking

スポンサーリンク