MOVES-Seminar, 30 May 2008, 14:00
Hierarchical Games for Model-Checking MSO over Natural Numbers.
Lukasz Kaiser, LuFGI 7
Abstract:
One approach to the verification of heap-manipulating programs is to
use logical interpretations: the structure on the heap is interpreted
in the natural numbers with successor or in the binary tree, and
properties of interest are translated to monadic second-order logic
over these structures. Complex properties can be expressed and checked
in this way, but current algorithms, based on automata techniques, are
too inefficient for practical use. We introduce a new representation
for MSO properties over natural numbers that is based on
model-checking games. These games are played by multiple players with
imperfect information exchanged according to a hierarchical
constraint, and the players form two coalitions with opposing
goals. We show that checking whether an MSO formula holds over natural
numbers can be reduced to the question which coalition wins in a
hierarchical game, and we discuss some ways to exploit the game
represenatation algorithmically.
use logical interpretations: the structure on the heap is interpreted
in the natural numbers with successor or in the binary tree, and
properties of interest are translated to monadic second-order logic
over these structures. Complex properties can be expressed and checked
in this way, but current algorithms, based on automata techniques, are
too inefficient for practical use. We introduce a new representation
for MSO properties over natural numbers that is based on
model-checking games. These games are played by multiple players with
imperfect information exchanged according to a hierarchical
constraint, and the players form two coalitions with opposing
goals. We show that checking whether an MSO formula holds over natural
numbers can be reduced to the question which coalition wins in a
hierarchical game, and we discuss some ways to exploit the game
represenatation algorithmically.
