2000 | OriginalPaper | Buchkapitel
A Unifying Approach to Data-Independence
verfasst von : Ranko Lazić, David Nowak
Erschienen in: CONCUR 2000 — Concurrency Theory
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.