A Game-Theoretic Approach to Simulation of Data-Parameterized Systems
=====================================================================

This work focuses on data-parameterized abstract systems that
extend standard modelling by allowing atomic propositions
to be parameterized by variables that range over some infinite domain.
These variables may range over process ids, message numbers, etc.

Thus, abstract systems enable simple modelling of infinite-state
systems whose source of infinity is the data.  We define and study a
simulation pre-order between abstract systems.  The definition extends
the definition of standard simulation by referring also to variable
assignments.  

We define $\vctl^\star$ -- an extension of $\ctl^\star$ by variables,
which is capable of specifying properties of abstract systems.  We
show that $\vctl^\star$ logically characterizes the simulation
pre-order between abstract systems.  That is, that satisfaction of
$\vactl^\star$, namely the universal fragment of $\vctl^\star$, is
preserved in simulating abstract systems.  For the second direction,
we show that if an abstract system ${\A}_2$ does not simulate an
abstract system ${\A}_1$, then there exists a $\vactl$ formula that
distinguishes ${\A}_1$ from ${\A}_2$.  Finally, we present a
game-theoretic approach to simulation of abstract systems and show
that the prover wins the game iff ${\A}_2$ simulates ${\A}_1$.
Further, if ${\A}_2$ does not simulate ${\A}_1$, then the refuter wins
the game and his winning strategy corresponds to a $\vactl$ formula
that distinguishes ${\A}_1$ from ${\A}_2$.  Thus, the many appealing
practical advantages of simulation are lifted to the setting of
data-parameterized abstract systems.