Mixed Simulation of Multi-valued Models

Multi-valued models, with additional logic values to capture the degree of uncertainty, support modeling and reasoning about systems with partial and inconsistent information. A mixed simulation, often used in abstract model checking, describes the connection between behaviors of two models and defines a precision order. In this paper, we derive a new notion of mixed simulation of multi-valued models such that the precision order is logically characterized by multi-valued semantics of propositional μ-calculus, it generalizes previous notion of mixed simulation for any multi-valued logic. Our work is based on bilattices, consisting of both a truth ordering and an information ordering. We first define the mixed simulation of multi-valued models over world-based bilattices using a model reduction approach, show the logical characterization result, and discuss three stronger variants of our notion. We then extend the result for any multi-valued logic through lattice embedding.