Continuous reachability in ordered data VAS
Data VAS is a finite set of finitely supported functions from ordered data set to , where k is a dimension. A configuration/marking is a finitely supported function from to . From a configuration there is a step to if there is a vector and an ordered preserving bijection (permutation) form to such that . The reachability relation is a transitive closure of the step relation. The reachability problem is undecidable, that is why we are looking for different relaxation of it. Continuous reachability is a continuous version of the reachability. First, markings are finitely/supported functions from to . Further there is a continuous step from to if there are: , an order preserving data permutation , and a factor such that . A transitive closure of continuous step is a continuous reachability relation.
