Latticed Simulation Relations and Games

Multi-valued Kripke structures are Kripke structures in which the
atomic propositions and the transitions are not Boolean and can take
values from some set. In particular, latticed Kripke structures, in
which the elements in the set are partially ordered, are useful in
abstraction, query checking, and reasoning about multiple view-points.
The challenges that formal methods involve in the Boolean setting are
carried over, and in fact increase, in the presence of multi-valued
systems and logics.  We lift to the latticed setting two basic notions
that have been proven useful in the Boolean setting. We first define
latticed simulation between latticed Kripke structures. The
relation maps two structures M_1 and M_2 to a lattice element that
essentially denotes the truth value of the statement "every behavior
of M_1 is also a behavior of M_2".  We show that latticed-simulation
is logically characterized by the universal fragment of latticed
\mu-calculus, and can be calculated in polynomial time. We then
proceed to defining latticed two-player games. Such games are played
along graphs in which each transition have a value in the lattice. The
value of the game essentially denotes the truth value of the statement
"the \join-player can force the game to computations that satisfy the
winning condition". An earlier definition of such games involved a
zig-zagged traversal of paths generated during the game. Our
definition involves a forward traversal of the paths, and it leads to
better understanding of multi-valued games. In particular, we prove a
min-max property for such games, and relate latticed simulation with
latticed games.