Data Independence with Generalised Predicate Symbols.
Ranko Lazić, Bill Roscoe · 1999
Where a concurrent system Impl is parameterised by a data type X with respect to which it is data independent, it is often possible to prove that Impl has a property Spec for all X by verifying it for a nite number of instantiations of X (a threshold collection). In this paper we show how to extend the denition of data independence for CSP to allow concurrent systems to include symbols representing generalised predicates, i.e. mappings from the type X to xed nite types such as the two-element type of booleans. Some of the main theorems that provide threshold collections, which were originally proved for data independence without these symbols, are revised for this extension. Keywords: data independence, symbolic execution, predicate symbols, model checking, CSP 1 Introduction As the technology of model checking advances and it is used in practical system developments, the greatest obstacle is the state explosion problem. For this reason, a considerable amount of eort is dire...