Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

On a Semantic Definition of Data Independence

Ranko LazićContact Information and David NowakContact Information

(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.

Contact Information Ranko Lazić
Email: Ranko.Lazic@dcs.warwick.ac.uk

Contact Information David Nowak
Email: David.Nowak@lsv.ens-cachan.fr
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.81 • Server: mpweb17
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)