2019  OriginalPaper  Buchkapitel Open Access
Continuous Reachability for Unordered Data Petri Nets is in PTime
Autoren: Utkarsh Gupta, Preey Shah, S. Akshay, Piotr Hofman
1 Introduction
2 Preliminaries
3 UDPN, Reachability and Its Variants: Our Main Results
4 Equivalent Formulation via Matrices
5 Bounding Number of Data Values Used in \({\mathbb {Q},\mathbb {Q}^{+}}\)run
5.1 Transformation of an \(\mathbb {X}\)run

\( uniformize \) takes an \(\mathbb {X}\)step and a nonempty set of data values \({\mathbb {E}}\) as input and produces an \(\mathbb {X}\)run, such that in the resultant run, the effect of the run for each data value in \({\mathbb {E}}\) is equal.

\( replace \) takes an \(\mathbb {X}\)step, a single data value \(\alpha ,\) and a nonempty set of data values \({\mathbb {E}}\) as input and outputs an \(\mathbb {X}\)step which doesn’t use data value \(\alpha \).

\(\forall \alpha \in col ({\mathcal {P}}) \setminus {\mathbb {E}}\), \({\mathcal {P}}'(\bullet ,\alpha ) = {\mathcal {P}}(\bullet ,\alpha )\).

\(\forall \alpha \in {\mathbb {E}}\), \({\mathcal {P}}'(\bullet ,\alpha ) = {\mathcal {P}}(\bullet ,next_{{\mathbb {E}}}(\alpha ))\), where \(next_{{\mathbb {E}}}(\alpha ) = \min (\{ \beta \in {\mathbb {E}}\mid \beta > \alpha \})\) if \(\{ \beta \in {\mathbb {E}}\mid \beta> \alpha \} > 0\) and \(\min ({\mathbb {E}})\) otherwise.