19.14 Continuous reachability in ordered data VAS

Data VAS is a finite set of finitely supported functions from ordered data set \(\mathbb{D}\) to \(\mathbb{Z}^k\), where k is a dimension. A configuration/marking is a finitely supported function from \(\mathbb{D}\) to \(\mathbb{N}^k\).

From a configuration \(m\) there is a step to \(m'\) if there is a vector \(x\in \text{VAS}\) and \(\pi\) an ordered preserving bijection (permutation) form \(\mathbb{D}\) to \(\mathbb{D}\) such that \(m+x\circ \pi=m'\). 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 \(\mathbb{D}\) to \(\mathbb{Q}_{\geq 0}^k\). Further there is a continuous step from \(m\) to \(m'\) if there are: \(x\in \text{VAS}\), an order preserving data permutation \(\pi\), and a factor \(a\in \mathbb{Q}_{\geq 0}\) such that \(m+a\cdot x\circ \pi=m'\). A transitive closure of continuous step is a continuous reachability relation.