On a Semantic Definition of Data Independence
Ranko Lazić5
and David Nowak6 
| (5) |
Department of Computer Science, University of Warwick, UK |
| (6) |
LSV, CNRS & ENS Cachan, France |
Abstract
A variety of results which enable model checking of important classes of infinite-state systems are based on exploiting the
property of data independence. The literature contains a number of definitions of variants of data independence, which are
given by syntactic restrictions in particular formalisms. More recently, data independence was defined for labelled transition
systems using logical relations, enabling results about data independent systems to be proved without reference to a particular
syntax. In this paper, we show that the semantic definition is sufficiently strong for this purpose. More precisely, it was
known that any syntactically data independent symbolic LTS denotes a semantically data independent family of LTSs, but here
we show that the converse also holds.
Keywords Data independence - definability - logical relations - nondeterminism
We acknowledge support from the EPSRC Standard Research Grant ‘Exploiting Data Independence’, GR/M32900. A part of this research
was done at the Oxford University Computing Laboratory.
Also affiliated to the Mathematical Institute, Belgrade. This author was supported in part by a grant from the Intel Corporation,
a Junior Research Fellowship from Christ Church, Oxford, and previously by a scholarship from Hajrija & Boris Vukobrat and
Copechim France SA.
References secured to subscribers.