Multi-Valued Modal Fixed Point Logics for Model Checking

作者：Nishizawa Koki^*

来源：IEICE Transactions on Information and Systems, 2010, E93D(8): 2036-2039.

DOI：10.1587/transinf.E93.D.2036

• fixed point logic
• De Morgan algebra
• Heyting algebra
• min-plus algebra

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-8