Model Checking with Multi-valued Logics

In multi-valued model checking, a temporal logic formula is interpreted relative to a structure not as a truth value but as a lattice element. In this paper we present new algorithms for multi-valued model checking. We first show how to reduce multi-valued model checking with any distributive DeMorgan lattice to standard, two-valued model checking. We then present a direct, automata-theoretic algorithm for multivalued model checking with logics as expressive as the modal mu-calculus. As part of showing correctness of the algorithm, we present a new fundamental result about extended alternating automata, a generalization of standard alternating automata.

• Type: Conference
• Year: 2004
• Where: ICALP
• Authors: Glenn Bruns, Patrice Godefroid
• Keywords: ICALP 2004, Model Checking, Multi-valued Model Checking, Theoretical Computer Science, Two-valued Model Checking