← All problems
Unverified

Continuous reachability in ordered data VAS

Data VAS is a finite set of finitely supported functions from ordered data set D\mathbb{D} to Zk\mathbb{Z}^k, where k is a dimension. A configuration/marking is a finitely supported function from D\mathbb{D} to Nk\mathbb{N}^k. From a configuration mm there is a step to m′m' if there is a vector x∈VASx\in \text{VAS} and π\pi an ordered preserving bijection (permutation) form D\mathbb{D} to D\mathbb{D} such that m+x∘π=m′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 D\mathbb{D} to Q≥0k\mathbb{Q}_{\geq 0}^k. Further there is a continuous step from mm to m′m' if there are: x∈VASx\in \text{VAS}, an order preserving data permutation π\pi, and a factor a∈Q≥0a\in \mathbb{Q}_{\geq 0} such that m+a⋅x∘π=m′m+a\cdot x\circ \pi=m'. A transitive closure of continuous step is a continuous reachability relation.

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu