Programming Research Group
Technical Report TR-4-00
A unifying approach to data-independence
Ranko Lazic and
David Nowak
June 2000, 30 pp.
Abstract
A concurrent system is data-independent with respect to a data type when
the only operation it can perform on values of that type is equality testing.
The system can also assign, input, nondeterministically choose, and output
such values. Based on this intuitive definition, syntactic restrictions
which ensure data-independence have been formulated for a variety of
different formalisms. However, it is difficult to see how these are related.
We present the first semantic definition of data-independence which allows
equality testing, and its extension which allows constant symbols and
predicate symbols. Both are special cases of a definition of when a family
of labelled transition systems is parametric. This provides a unified
approach to data-independence and its extensions.
The paper also contains two theorems which, given a system and
a specification which are data-independent, enable the verification
for all instantiations of the data types (and of the constant symbols
and the predicate symbols, in the case of the extension) to be reduced
to the verification for a finite number of finite instantiations.
We illustrate the applicability of the approach to particular formalisms
by a programming language similar to UNITY, and by linear-time temporal
logic.
This paper is available as a 150840 gzipped PostScript file.