Continuous Reachability for Unordered Data Petri nets is in PTime

TL;DR

This paper proves that the continuous reachability problem for unordered data Petri nets can be decided in polynomial time, providing a new efficient method for analyzing these complex models.

Contribution

The authors characterize continuous reachability for UDPN and develop a polynomial time algorithm based on a combinatorial argument.

Findings

Continuous reachability for UDPN is in PTime.

Existence of runs with only polynomially many data values when reachability holds.

Provides a polynomial time decision procedure for continuous reachability.

Abstract

Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly complex, and its decidability status remains open. In this paper, we consider the continuous reachability problem for UDPN, which can be seen as an over-approximation of the reachability problem. Our main result is a characterization of continuous reachability for UDPN and polynomial time algorithm for solving it. This is a consequence of a combinatorial argument, which shows that if continuous reachability holds then there exists a run using only polynomially many data values.

Equations

$$(f+g)(x)=\begin{cases*}f(x)&if $x\in X_{1}\setminus X_{2}$\\ g(x)&if $x\in X_{2}\setminus X_{1}$\\ f(x)+g(x)&if $x\in X_{1}\cap X_{2}$.\end{cases*}$$

$${{{\textbf{{i}}}}}=\ \blockarray{ccccc}red&bluegreenblack\\ \block{(cccc)c}1010\ \ p_{1}\\ 0100\ \ p_{2}\\ 2000\ \ p_{3}\\ 1100\ \ p_{4}\\ \quad{\Delta(t)}=\blockarray{cccc}x&yz\\ \block{(ccc)c}0-10\ \ p_{1}\\ -100\ \ p_{2}\\ 020\ \ p_{3}\\ 101\ \ p_{4}\\$$

$$\vbox{ \scalebox{0.9}{ \leavevmode\hbox to91.85pt{\vbox to96.43pt{\pgfpicture\makeatletter\hbox{\hskip 82.913pt\lower-74.37717pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } \par\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{}\pgfsys@moveto{8.53583pt}{0.0pt}\pgfsys@curveto{8.53583pt}{4.71426pt}{4.71426pt}{8.53583pt}{0.0pt}{8.53583pt}\pgfsys@curveto{-4.71426pt}{8.53583pt}{-8.53583pt}{4.71426pt}{-8.53583pt}{0.0pt}\pgfsys@curveto{-8.53583pt}{-4.71426pt}{-4.71426pt}{-8.53583pt}{0.0pt}{-8.53583pt}\pgfsys@curveto{4.71426pt}{-8.53583pt}{8.53583pt}{-4.71426pt}{8.53583pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.91562pt}{14.41325pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{2}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{{}}}}{{}}{{}}{{}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@fill{0.8}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,0.25}\pgfsys@color@gray@stroke{0.25}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,0.8}\pgfsys@color@gray@fill{0.8}\pgfsys@invoke{ }{}\pgfsys@rect{-42.67914pt}{-34.86116pt}{11.3811pt}{12.8168pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-38.93303pt}{-31.52815pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{t}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-29.31285pt}{-22.54926pt}\pgfsys@lineto{-7.08269pt}{-5.44826pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-0.7926}{-0.60973}{0.60973}{-0.7926}{-29.31285pt}{-22.54924pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-27.80118pt}{-11.07547pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{x}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{ {}{}{}}}}{{}}{{}}{{}}{{{{}}}}{} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{}\pgfsys@moveto{-65.44135pt}{0.0pt}\pgfsys@curveto{-65.44135pt}{4.71426pt}{-69.26291pt}{8.53583pt}{-73.97717pt}{8.53583pt}\pgfsys@curveto{-78.69144pt}{8.53583pt}{-82.513pt}{4.71426pt}{-82.513pt}{0.0pt}\pgfsys@curveto{-82.513pt}{-4.71426pt}{-78.69144pt}{-8.53583pt}{-73.97717pt}{-8.53583pt}\pgfsys@curveto{-69.26291pt}{-8.53583pt}{-65.44135pt}{-4.71426pt}{-65.44135pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{-73.97717pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-73.97717pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@moveto{-71.8244pt}{0.0pt}\pgfsys@curveto{-71.8244pt}{1.18895pt}{-72.78822pt}{2.15277pt}{-73.97717pt}{2.15277pt}\pgfsys@curveto{-75.16612pt}{2.15277pt}{-76.12994pt}{1.18895pt}{-76.12994pt}{0.0pt}\pgfsys@curveto{-76.12994pt}{-1.18895pt}{-75.16612pt}{-2.15277pt}{-73.97717pt}{-2.15277pt}\pgfsys@curveto{-72.78822pt}{-2.15277pt}{-71.8244pt}{-1.18895pt}{-71.8244pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{-73.97717pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-73.97717pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-77.89279pt}{14.41325pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{1}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-66.89462pt}{-5.44867pt}\pgfsys@lineto{-44.66432pt}{-22.55043pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.7926}{-0.60974}{0.60974}{0.7926}{-44.66432pt}{-22.55043pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-51.45387pt}{-9.13185pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{y}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{{{}}}}{{}}{{}}{{}}{{{{}}}}{}{}{}{}\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{}\pgfsys@moveto{8.53583pt}{-65.44135pt}\pgfsys@curveto{8.53583pt}{-60.72708pt}{4.71426pt}{-56.90552pt}{0.0pt}{-56.90552pt}\pgfsys@curveto{-4.71426pt}{-56.90552pt}{-8.53583pt}{-60.72708pt}{-8.53583pt}{-65.44135pt}\pgfsys@curveto{-8.53583pt}{-70.15561pt}{-4.71426pt}{-73.97717pt}{0.0pt}{-73.97717pt}\pgfsys@curveto{4.71426pt}{-73.97717pt}{8.53583pt}{-70.15561pt}{8.53583pt}{-65.44135pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-65.44135pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-65.44135pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@moveto{-1.07639pt}{-62.21219pt}\pgfsys@curveto{-1.07639pt}{-61.02324pt}{-2.0402pt}{-60.05942pt}{-3.22916pt}{-60.05942pt}\pgfsys@curveto{-4.4181pt}{-60.05942pt}{-5.38193pt}{-61.02324pt}{-5.38193pt}{-62.21219pt}\pgfsys@curveto{-5.38193pt}{-63.40114pt}{-4.4181pt}{-64.36496pt}{-3.22916pt}{-64.36496pt}\pgfsys@curveto{-2.0402pt}{-64.36496pt}{-1.07639pt}{-63.40114pt}{-1.07639pt}{-62.21219pt}\pgfsys@closepath\pgfsys@moveto{-3.22916pt}{-62.21219pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.22916pt}{-62.21219pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,1}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{5.38193pt}{-62.21219pt}\pgfsys@curveto{5.38193pt}{-61.02324pt}{4.4181pt}{-60.05942pt}{3.22916pt}{-60.05942pt}\pgfsys@curveto{2.0402pt}{-60.05942pt}{1.07639pt}{-61.02324pt}{1.07639pt}{-62.21219pt}\pgfsys@curveto{1.07639pt}{-63.40114pt}{2.0402pt}{-64.36496pt}{3.22916pt}{-64.36496pt}\pgfsys@curveto{4.4181pt}{-64.36496pt}{5.38193pt}{-63.40114pt}{5.38193pt}{-62.21219pt}\pgfsys@closepath\pgfsys@moveto{3.22916pt}{-62.21219pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.22916pt}{-62.21219pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,1}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{-1.07639pt}{-68.6705pt}\pgfsys@curveto{-1.07639pt}{-67.48155pt}{-2.0402pt}{-66.51773pt}{-3.22916pt}{-66.51773pt}\pgfsys@curveto{-4.4181pt}{-66.51773pt}{-5.38193pt}{-67.48155pt}{-5.38193pt}{-68.6705pt}\pgfsys@curveto{-5.38193pt}{-69.85945pt}{-4.4181pt}{-70.82327pt}{-3.22916pt}{-70.82327pt}\pgfsys@curveto{-2.0402pt}{-70.82327pt}{-1.07639pt}{-69.85945pt}{-1.07639pt}{-68.6705pt}\pgfsys@closepath\pgfsys@moveto{-3.22916pt}{-68.6705pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.22916pt}{-68.6705pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@moveto{5.38193pt}{-68.6705pt}\pgfsys@curveto{5.38193pt}{-67.48155pt}{4.4181pt}{-66.51773pt}{3.22916pt}{-66.51773pt}\pgfsys@curveto{2.0402pt}{-66.51773pt}{1.07639pt}{-67.48155pt}{1.07639pt}{-68.6705pt}\pgfsys@curveto{1.07639pt}{-69.85945pt}{2.0402pt}{-70.82327pt}{3.22916pt}{-70.82327pt}\pgfsys@curveto{4.4181pt}{-70.82327pt}{5.38193pt}{-69.85945pt}{5.38193pt}{-68.6705pt}\pgfsys@closepath\pgfsys@moveto{3.22916pt}{-68.6705pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.22916pt}{-68.6705pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\hbox{\tiny{\definecolor[named]{.}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-7.73245pt}{-57.70824pt}\pgfsys@lineto{-30.89804pt}{-34.54051pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{0.70708}{-0.70714}{0.70714}{0.70708}{-7.73245pt}{-57.70822pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{}}{} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-34.6412pt}{-54.67006pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{x,z}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{{{}}}}{{}}{{}}{{}}{{{{}}}}{}{}{}{} {{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{{ }}}\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0.25,0.25,1}\pgfsys@color@rgb@stroke{0.25}{0.25}{1}\pgfsys@invoke{ }\definecolor{pgffillcolor}{rgb}{0.8,0.8,1}\pgfsys@color@rgb@fill{0.8}{0.8}{1}\pgfsys@invoke{ }{}\pgfsys@moveto{-65.44135pt}{-65.44135pt}\pgfsys@curveto{-65.44135pt}{-60.72708pt}{-69.26291pt}{-56.90552pt}{-73.97717pt}{-56.90552pt}\pgfsys@curveto{-78.69144pt}{-56.90552pt}{-82.513pt}{-60.72708pt}{-82.513pt}{-65.44135pt}\pgfsys@curveto{-82.513pt}{-70.15561pt}{-78.69144pt}{-73.97717pt}{-73.97717pt}{-73.97717pt}\pgfsys@curveto{-69.26291pt}{-73.97717pt}{-65.44135pt}{-70.15561pt}{-65.44135pt}{-65.44135pt}\pgfsys@closepath\pgfsys@moveto{-73.97717pt}{-65.44135pt}\pgfsys@fillstroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-73.97717pt}{-65.44135pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@moveto{-75.05356pt}{-62.21219pt}\pgfsys@curveto{-75.05356pt}{-61.02324pt}{-76.01738pt}{-60.05942pt}{-77.20633pt}{-60.05942pt}\pgfsys@curveto{-78.39528pt}{-60.05942pt}{-79.3591pt}{-61.02324pt}{-79.3591pt}{-62.21219pt}\pgfsys@curveto{-79.3591pt}{-63.40114pt}{-78.39528pt}{-64.36496pt}{-77.20633pt}{-64.36496pt}\pgfsys@curveto{-76.01738pt}{-64.36496pt}{-75.05356pt}{-63.40114pt}{-75.05356pt}{-62.21219pt}\pgfsys@closepath\pgfsys@moveto{-77.20633pt}{-62.21219pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-77.20633pt}{-62.21219pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@moveto{-68.59525pt}{-62.21219pt}\pgfsys@curveto{-68.59525pt}{-61.02324pt}{-69.55907pt}{-60.05942pt}{-70.74802pt}{-60.05942pt}\pgfsys@curveto{-71.93697pt}{-60.05942pt}{-72.90079pt}{-61.02324pt}{-72.90079pt}{-62.21219pt}\pgfsys@curveto{-72.90079pt}{-63.40114pt}{-71.93697pt}{-64.36496pt}{-70.74802pt}{-64.36496pt}\pgfsys@curveto{-69.55907pt}{-64.36496pt}{-68.59525pt}{-63.40114pt}{-68.59525pt}{-62.21219pt}\pgfsys@closepath\pgfsys@moveto{-70.74802pt}{-62.21219pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-70.74802pt}{-62.21219pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,1,0}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,1,0}\pgfsys@moveto{-75.05356pt}{-68.6705pt}\pgfsys@curveto{-75.05356pt}{-67.48155pt}{-76.01738pt}{-66.51773pt}{-77.20633pt}{-66.51773pt}\pgfsys@curveto{-78.39528pt}{-66.51773pt}{-79.3591pt}{-67.48155pt}{-79.3591pt}{-68.6705pt}\pgfsys@curveto{-79.3591pt}{-69.85945pt}{-78.39528pt}{-70.82327pt}{-77.20633pt}{-70.82327pt}\pgfsys@curveto{-76.01738pt}{-70.82327pt}{-75.05356pt}{-69.85945pt}{-75.05356pt}{-68.6705pt}\pgfsys@closepath\pgfsys@moveto{-77.20633pt}{-68.6705pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-77.20633pt}{-68.6705pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,1,0}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{ }\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{ }\definecolor[named]{pgffillcolor}{rgb}{0,1,0}\pgfsys@moveto{-68.59525pt}{-68.6705pt}\pgfsys@curveto{-68.59525pt}{-67.48155pt}{-69.55907pt}{-66.51773pt}{-70.74802pt}{-66.51773pt}\pgfsys@curveto{-71.93697pt}{-66.51773pt}{-72.90079pt}{-67.48155pt}{-72.90079pt}{-68.6705pt}\pgfsys@curveto{-72.90079pt}{-69.85945pt}{-71.93697pt}{-70.82327pt}{-70.74802pt}{-70.82327pt}\pgfsys@curveto{-69.55907pt}{-70.82327pt}{-68.59525pt}{-69.85945pt}{-68.59525pt}{-68.6705pt}\pgfsys@closepath\pgfsys@moveto{-70.74802pt}{-68.6705pt}\pgfsys@fill\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-70.74802pt}{-68.6705pt}\pgfsys@invoke{ }\hbox{{\definecolor[named]{.}{rgb}{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}\pgfsys@stroke\pgfsys@invoke{ } }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-77.89279pt}{-51.02809pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$p_{3}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{-66.24472pt}{-57.70824pt}\pgfsys@lineto{-43.07913pt}{-34.54051pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-0.70708}{-0.70714}{0.70714}{-0.70708}{-66.24472pt}{-57.70822pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ }}{ } {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-79.16364pt}{-40.79851pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\{2y\}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{M_{{\textbf{{f}}}}=\blockarray{ccccc}red&bluegreenblack\\ \block{(cccc)c}1000\ \ p_{1}\\ 0000\ \ p_{2}\\ 2020\ \ p_{3}\\ 1201\ \ p_{4}\\ {\mathcal{P}}=\blockarray{cccc}&bluegreenblack\\ \block{c(ccc)}x\ \ 100\\ y\ \ 010\\ z\ \ 001\\ }\\$$

$$\mathcal{R}(\alpha ,\mathbb{E},\omega )=\{\begin{array}{ll}(c,t,\mathcal{P})& \text{if }(\Delta (t)\cdot \mathcal{P})(\bullet ,\alpha )=\text{0}\\ (c,t,swa{p}_{\alpha ,\beta }(\mathcal{P}))& \text{otherwise, }\text{where }\beta \text{ is a smallest}\\ & \text{datum ∈E such that }(\Delta (t)\cdot \mathcal{P})(\bullet ,\beta )=\text{0}\end{array}$$

$$\mathcal{U}(\mathbb{E},\mathcal{R}(\alpha ,\mathbb{E},\sigma (1)))\text{leavevmode}\text{c◯}\text{leavevmode}\mathcal{U}(\mathbb{E},\mathcal{R}(\alpha ,\mathbb{E},\sigma (2)))\text{leavevmode}\text{c◯}\text{leavevmode}...\text{leavevmode}\text{c◯}\text{leavevmode}\mathcal{U}(\mathbb{E},\mathcal{R}(\alpha ,\mathbb{E},\sigma (|\sigma |))).$$

$$\text{i}={\text{m}}_0{\stackrel{{\sigma }_1}{\to }}_{\mathbb{X}}{\text{m}}_1{\stackrel{{\sigma }_2}{\to }}_{\mathbb{X}}{\text{m}}_2{\stackrel{{\sigma }_3}{\to }}_{\mathbb{X}}\dots {\stackrel{{\sigma }_l}{\to }}_{\mathbb{X}}{\text{m}}_l=\text{f}$$

$$\text{i}={\text{m}}_o^{\prime }{\stackrel{\mathcal{U}(\mathbb{E},\mathcal{R}(\alpha ,\mathbb{E},{\sigma }_1))}{\to }}_{\mathbb{Q}}{\text{m}}_1^{\prime }{\stackrel{\mathcal{U}(\mathbb{E},\mathcal{R}(\alpha ,\mathbb{E},{\sigma }_2))}{\to }}_{\mathbb{Q}}{\text{m}}_2^{\prime }\dots {\stackrel{\mathcal{U}(\mathbb{E},\mathcal{R}(\alpha ,\mathbb{E},{\sigma }_l))}{\to }}_{\mathbb{Q}}{\text{m}}_l^{\prime }={\text{f}}^{\prime }$$

$$\frac{1}{|\mathbb{E}|}\sum _{k=0}^{|\mathbb{E}|-1}\Delta ({rot}^k(\mathbb{E},\mathcal{R}(\alpha ,\mathbb{E},\omega )))(\bullet ,\gamma )=\frac{1}{|\mathbb{E}|}\sum _{k=0}^{|\mathbb{E}|}\Delta ({rot}^k(\mathbb{E}\cup \{\alpha \},\omega ))(\bullet ,\gamma )$$

$$=\frac{c_j}{|\mathbb{E}|}\sum _{k=0}^{|\mathbb{E}|}({rot}^k(F(\bullet ,t_j)\cdot {\mathcal{P}}_j))(\bullet ,\delta )=\frac{c_j}{|\mathbb{E}|}\sum _{\delta \in \mathbb{E}\cup \{\alpha \}}(F(\bullet ,t_j)\cdot {\mathcal{P}}_j)(\bullet ,\delta ).$$

$$c_j(F(\bullet ,t_j)\cdot {\mathcal{P}}_j)(\bullet ,\delta )\le {\text{m}}_j(\bullet ,\delta )\text{ for all }\delta \in \mathbb{D},$$

$$\frac{1}{|\mathbb{E}|}{c}_j\sum _{\delta \in \mathbb{E}\cup \{\alpha \}}(F(\bullet ,t_j)\cdot {\mathcal{P}}_j)(\bullet ,\delta )\le \frac{1}{|\mathbb{E}|}\sum _{\delta \in \mathbb{E}\cup \{\alpha \}}{\text{m}}_j(\bullet ,\delta )={\text{m}}_j^{\prime }(\delta ,\gamma ),$$

$$\sum _{\alpha \in \mathbb{Y}}{h}_i[r][\alpha ]=\sum _{\alpha \in \mathbb{Y}}{h}_i[1][\alpha ]\text{ and }\sum _{r\in Var}{h}_i[r][\alpha ]\le \sum _{\beta \in \mathbb{Y}}{h}_i[1][\beta ].$$

$$\begin{array}{rl}(4)& F(p,t_i)(r)<0\text{leavevmode}\wedge \text{leavevmode}{h}_i[r][\alpha ]>0\text{leavevmode}⟹\text{leavevmode}{\text{i}}^{\prime }(p,\alpha )>0\\ (5)& F(t_i,p)(r)>0\text{leavevmode}\wedge \text{leavevmode}{h}_i[r][\alpha ]>0\text{leavevmode}⟹\text{leavevmode}{\text{f}}^{\prime }(p,\alpha )>0\end{array}$$

$$\left[(t_1,h_{1,1})(t_2,h_{2,1})\dots (t_{|T|},h_{|T|,1})\right]\dots \left[(t_1,h_{1,B})\dots (t_{|T|},h_{|T|,B})\right]$$

$$\begin{array}{rl}{\text{f}}^{\prime }(\bullet ,\alpha )-{\text{i}}^{\prime }(\bullet ,\alpha )& =\sum _{j=0}^{|\mathbb{E}|-1}\Delta ({rot}^j(\mathbb{E},\frac{\omega }{|\mathbb{E}|}))(\bullet ,\alpha )=\frac{c}{|\mathbb{E}|}\left(\sum _{j=0}^{|\mathbb{E}|-1}(\Delta (t)\cdot \mathcal{P})(\bullet ,\alpha )\right)\\ & =c\Delta (t)\cdot \mathcal{P}(\bullet ,\alpha )=\text{f}(\bullet ,\alpha )-\text{i}(\bullet ,\alpha )\end{array}$$

$$\begin{array}{rl}\sum _{j=0}^{|\mathbb{E}|-1}\Delta ({rot}^j(\mathbb{E},\frac{\omega }{|\mathbb{E}|}))(\bullet ,\alpha )=& \frac{c}{|\mathbb{E}|}\left(\sum _{j=0}^{|\mathbb{E}|-1}(\Delta (t)\cdot \mathcal{P})(\bullet ,nex{t}_{\mathbb{E}}^j(\alpha ))\right)\\ =\frac{c}{|\mathbb{E}|}\left(\sum _{\beta \in \mathbb{E}}(\Delta (t)\cdot \mathcal{P})(\bullet ,\beta )\right)=& \frac{{\sum }_{\beta \in \mathbb{E}}(\text{f}(\bullet ,\beta )-\text{i}(\bullet ,\beta ))}{|\mathbb{E}|}\end{array}$$

$$\text{z}(\bullet ,\gamma )={\text{m}}_{j+1}^{\prime }(\bullet ,\gamma )\text{ for all }\gamma \in dval(\text{i})\cup dval(\text{f}).$$

$$\begin{array}{r}{\text{m}}_{j+1}^{\prime }(\bullet ,\gamma )-{\text{m}}_j^{\prime }(\bullet ,\gamma )=\frac{1}{|\mathbb{E}|}\left(\sum _{\delta \in \mathbb{E}}\left({\text{z}}^{\prime }(\bullet ,\delta )-{\text{m}}_j^{\prime }(\bullet ,\delta )\right)\right)=\\ \frac{1}{|\mathbb{E}|}\left(\text{z}(\bullet ,\beta )+\text{z}(\bullet ,\alpha )+\sum _{\delta \in \mathbb{E}\setminus \{\alpha ,\beta \}}\text{z}(\bullet ,\delta )-\sum _{\delta \in \mathbb{E}}{\text{m}}_j^{\prime }(\bullet ,\delta )\right)=\\ \frac{1}{|\mathbb{E}|}\left(\sum _{\delta \in \mathbb{E}\cup \{\alpha \}}\text{z}(\bullet ,\delta )-\sum _{\delta \in \mathbb{E}}{\text{m}}_j^{\prime }(\bullet ,\delta )\right)\end{array}$$

$$\begin{array}{r}\frac{{\sum }_{\delta \in \mathbb{E}\cup \{\alpha \}}\text{z}(\bullet ,\delta )-{\sum }_{\delta \in \mathbb{E}\cup \{\alpha \}}{\text{m}}_j^{\prime }(\bullet ,\delta )}{|\mathbb{E}|}=\frac{{\sum }_{\delta \in \mathbb{E}\cup \{\alpha \}}({\text{m}}_{j+1}(\bullet ,\delta )-{\text{m}}_j(\bullet ,\delta ))}{|\mathbb{E}|}.\end{array}$$

$$\begin{array}{r}\frac{{\sum }_{\delta \in \mathbb{E}\cup \{\alpha \}}{\text{m}}_{j+1}(\bullet ,\delta )-{\sum }_{\delta \in \mathbb{E}}{\text{m}}_j(\bullet ,\delta )}{|\mathbb{E}|}=\frac{{\sum }_{\delta \in \mathbb{E}\cup \{\alpha \}}{\text{m}}_{j+1}(\bullet ,\delta )}{|\mathbb{E}|}-{\text{m}}_j^{\prime }(\bullet ,\gamma ),\end{array}$$

$$\sum _{\alpha \in col(H_0)}{H}_0(x,\alpha )=\sum _{i=1}^n\sum _{\alpha \in col(H_i)}{H}_i(x,\alpha )=\sum _{i=1}^n{q}_i.$$

$$\sum _{x\in row(H_0)}{H}_0(x,\alpha )=\sum _{i=1}^n\sum _{x\in row(H_0)}{H}_i(x,\alpha )\le \sum _{i=1}^n{q}_i$$

$$\omega =\sum _{i=1}^{|\sigma |}\sum _{p\in P}\sum _{x\in vars(t_i)}{c}_i\cdot (F(t_i,p)(x)+F(p,t_i)(x))$$

$$c=\min \{\text{i}(p,\alpha ),\text{f}(p,\beta ):(p,\alpha )\in Pre(\sigma ),(p,\beta )\in Post(\sigma )\}.$$

$$\text{i}{\stackrel{\frac{\sigma }{n}}{\to }}_{\mathbb{Q}}{\text{m}}_1{\stackrel{\frac{\sigma }{n}}{\to }}_{\mathbb{Q}}{\text{m}}_2...{\text{m}}_{n-1}{\stackrel{\frac{\sigma }{n}}{\to }}_{\mathbb{Q}}\text{f}.$$

$$\begin{array}{r}\omega =\frac{\min (\{\text{i}(p,\alpha )>0,\text{f}(p,\alpha )>0:p\in P,\alpha \in \mathbb{D}\}\cup }{\max (\{\text{i}(p,\alpha )>0,\text{f}(p,\alpha )>0:p\in P,\alpha \in \mathbb{D}\}\cup }\\ \frac{F(t,p)(x)>0,F(p,t)(x)>0:t\in T,x\in vars(t),p\in P\})}{\{F(t,p)(x)>0,F(p,t)(x)>0:t\in T,x\in vars(t),p\in P\})}.\end{array}$$

$${\omega }_{prev}=c_{min}\cdot \left(\frac{\omega }{2}\right),c_{min}\cdot {\left(\frac{\omega }{2}\right)}^2,c_{min}\cdot {\left(\frac{\omega }{2}\right)}^3\dots c_{min}\cdot {\left(\frac{\omega }{2}\right)}^{|{\mathbb{S}}_{prev}|}\text{ and }$$

$${\omega }_{post}=c_{min}\cdot {\left(\frac{\omega }{2}\right)}^{|{\mathbb{S}}_{post}|},c_{min}\cdot {\left(\frac{\omega }{2}\right)}^{|{\mathbb{S}}_{post}|-1},c_{min}\cdot {\left(\frac{\omega }{2}\right)}^{|{\mathbb{S}}_{post}|-2}\dots c_{min}\cdot \left(\frac{\omega }{2}\right).$$

Full text

1 Introduction

The theory of Petri Nets has been developing since more than 50 years. On one hand, from a theory perspective, Petri Nets are interesting due to their deep mathematical structure and despite exhibiting nice properties, like being a well structured transition system [1], we still don’t understand them well. On the other hand, Petri Nets are a useful pictorial formalism for modeling and thus found their way to the industry. To connect this theory and practice, it would be desirable to use the developed theory of Petri Nets [2, 3, 4] for the symbolic analysis and verification of Petri Nets models. However, we already know that this is difficult in its full generality. It suffices to recall two results that were proved more than 30 years apart. An old but classical result by Lipton [5] shows that even coverability is ExpSpace-hard, while the non-elementary hardness of the reachability relation has just been established this year [6]. Moreover, when we look at Petri nets based formalisms that are needed to model various aspects of industrial systems, we see that they go beyond the expressivity of Petri Nets. For instance, colored Petri nets, which are used in modeling workflows [7], allow the tokens to be colored with an infinite set of colors, and introduce a complex formalism to describe dependencies between colors. This makes all verification problems undecidable for this generic model. Given the basic nature and importance of the reachability problem in Petri nets (and its extensions), there have been several efforts to sidestep the complexity-theoretic hardness results. One common approach is to look for easy subclasses (such as bounded nets [8], free-choice nets [9] etc). The other approach, which we adopt in this work, is to compute over-approximations of the reachability relation.

Continuous reachability. A natural question regarding the dynamics of a Petri net is to ask what would happen if tokens instead of behaving like discrete units start to behave like a continuous fluid? This simple question led us to an elegant theory of so-called continuous Petri nets [10, 11, 12]. Petri nets with continuous semantics allow markings to be functions from places to nonnegative rational numbers (i.e., in $\mathbb{Q}^{+}$) instead of natural numbers. Moreover, whenever a transition is fired a positive rational coefficient is chosen and both the number of consumed and produced tokens are multiplied with the coefficient. This allows to split tokens into arbitrarily small parts and process them independently. This for instance may occur in applications related to hybrid systems where the discrete part is used to control the continuous systems [13, 14]. Interestingly, this makes things simpler to analyze. For example reachability under the continuous semantics for Petri nets is $PTime$-complete [11].

However, when one wants to analyze extensions of Petri nets, for example reset Petri Nets with continuous semantics, it turns out that reachability is as hard as reachability in reset Petri nets under the usual semantics i.e. it is undecidable111This can be seen on the same lines as the proof of undecidability of continuous reachability for Petri nets with zero tests [12].. In this paper we identify an extension of Petri nets with unordered data, for which this is not the case and continuous semantics leads to a substantial reduction in the complexity of the reachability problem.

Unordered data Petri Nets. The possibility of equipping tokens with some additional information is one of the main lines of research regarding extensions of Petri Nets, the best known being Colored Petri Nets [15] and various types of timed Petri Nets [16, 17]. In [18] authors equipped tokens with data and restricted interactions between data in a way that allow to transfer techniques for well structured transition systems. They identified various classes of nets exhibiting interesting combinatorial properties which led to a number of results [19, 20, 21, 22, 23]. Unordered Data Petri Nets (UDPN), are simplest among them: every token carries a single datum like a barcode and transitions may check equality or disequality of data in consumed and produced tokens. UDPN are the only class identified in [18] for which the reachability is still unsolved, although in [20] authors show that the problem is at least Ackermannian-hard (for all other data extensions, reachability is undecidable). A recent attempt to over-approximate the reachability relation for UDPN in [22] considers integer reachability i.e. number of tokens may get negative during the run (also called solution of the state equation). From the above perspective, this paper is an extension of the mentioned line of research.

Our contribution. Our main contribution is a characterization of continuous reachability in UDPN and a polynomial time algorithm for solving it. Observe that if we find an upper bound on the minimal number of data required by a run between two configurations (if any run exists), then we can reduce continuous reachability in UDPN to continuous reachability in vanilla Petri nets with an exponential blowup and use the already developed characterization from [11]. In Section 5 we prove such a bound on the minimal number of required data. The bound is novel and exploits techniques that did not appear previously in the context of data nets. Further, the obtained bounds are lower than bounds on the number of data values required to solve the state equation [22], which is surprising considering that existence of a continuous run requires a solution of a sort of state equation. Precisely, the difference is that we are looking for solutions of the state equation over $\mathbb{Q}^{+}$ instead of $\mathbb{N}$ and in this case we prove better bounds for the number of data required. This also gives us an easy polytime algorithm for finding $\mathbb{Q}^{+}$-solutions of state equations of UDPN (we remark that for Petri nets without data, this appears among standard algebraic techniques  [24]).

Finally, with the above bound, we solve continuous reachability in UDPN by adapting the techniques from the non-data setting of [12, 25]. We adapt the characterization of continuous reachability to the data setting and next encode it as system of linear equations with implications. In doing so, however, we face the problem that a naive encoding (representing data explicitly) gives a system of equations of exponential size, giving only an ExpTime-algorithm. To improve the complexity, we use histograms, a combinatorial tool developed in [22], to compress the description of solutions of state equations in UDPNs. However, this may lead to spurious solutions for continuous reachability. To eliminate them, we show that it suffices to first transform the net and then apply the idea of histograms to characterize continuous runs in the modified net. The whole procedure is described in Section 7.3 and leads us to our $PTime$ algorithm for continuous reachability in UDPN. Note that since we easily have $PTime$ hardness for the problem (even without data), we obtain that the problem of continuous reachability in UDPN is $PTime$-complete.

Towards verification. Over-approximations are useful in verification of Petri nets and their extensions: as explained in [24], for many practical problems, over-approximate solutions are already correct. Further, we can use them as a sub-routine to improve the practical performance of verification algorithms. A remarkable example is the recent work in [25], where the $PTime$ continuous reachability algorithm for Petri nets from [11] is used as a subroutine to solve the $ExpSpace$ hard coverability problem in Petri nets, outperforming the best known tools for this problem, such as Petrinizer [26]. Our results can be seen as a first step in the same spirit towards handling practical instances of coverability, but for the extended model of UDPN, where the coverability problem for UDPN is known to be Ackermannian-hard [20].

2 Preliminaries

We denote integers, non-negative integers, rationals, and reals as $\mathbb{Z},\mathbb{N},\mathbb{Q},$ and $\mathbb{R}$, respectively. For a set $\mathbb{X}\subseteq\mathbb{R}$ denote by $\mathbb{X}^{+}$, the set of all non-negative elements of $\mathbb{X}$. We denote by 0, a vector whose entries are all zero. We define in a standard point-wise way operations on vectors i.e. scalar multiplication $\cdot$, addition $+$, subtraction $-$, and vector comparison $\leq$. In this paper, we use functions of the type $X\to(Y\to Z)$, and instead of $(f(x))(y)$, we write $f(y,x).$ For functions $f,g$ where the range of $g$ is a subset of the domain of $f$, we denote their composition by $f\circ g$. If $\pi$ is an injection then by $\pi^{-1}$ we mean a partial function such that $\pi^{-1}\circ\pi$ is the identity function. Let $f:X_{1}\to Y$ , $g:X_{2}\to Y$ be two functions with addition and scalar multiplication operations defined on $Y.$ A scalar multiplication of a function is defined as follows $(a\cdot f)(x)=a\cdot f(x)$ for all $x\in X_{1}.$ We lift addition operation to functions pointwise, i.e. $f+g:X_{1}\cup X_{2}\to Y$ such that

[TABLE]

Similarly for subtraction $(f-g)(x)=f(x)+-1\cdot g(x)$.

We use matrices with rows and columns indexed by sets $\mathbb{S}_{1},\mathbb{S}_{2}$, possibly infinite. For a matrix $M$, let $M(r,c)$ denote the entry at column $c$ and row $r$, and $M(r,\bullet)$,$M(\bullet,c)$ denote the row vector indexed by $r$ and column vector indexed by $c$, respectively. Denote by $\mathit{col}(M)$, $\mathit{row}(M)$ the set of indices of nonzero columns and nonzero rows of the matrix $M$, respectively. Even if we have infinitely many rows or columns, our matrices will have only finitely many nonzero rows and columns, and only this nonzero part will be represented. Following our nonstandard matrix definition we precisely define operations on them, although they are natural. First, a multiplication by a constant number produces a new matrix with row and columns labelled with the same sets $\mathbb{S}_{1},\mathbb{S}_{2}$ and defined as follows $(a\cdot M)(r,c)=a\cdot(M(r,c))$ for all $(r,c)\in\mathbb{S}_{1}\times\mathbb{S}_{2}$. Addition of two matrices is only defined if the sets indexing rows $\mathbb{S}_{1}$ and columns $\mathbb{S}_{2}$ are the same for both summands $M_{1}$ and $M_{2}$, $\forall(r,c)\in\mathbb{S}_{1}\times\mathbb{S}_{2}$ the sum $(M_{1}+M_{2})(r,c)=M_{1}(r,c)+M_{2}(r,c)$, the subtraction $M_{1}-M_{2}$ is a shorthand for $M_{1}+(-1)\cdot M_{2}$. Observe that all but finitely many entries in matrices are [math], and therefore when we do computation on matrices we can restrict to rows $\mathit{row}(M_{1})\cup\mathit{row}(M_{2})$ and columns $\mathit{col}(M_{1})\cup\mathit{col}(M_{2})$. Similarly the comparison for two matrices $M_{1},M_{2}$ is defined as follows $M_{1}\leq M_{2}$ if $\forall(r,c)\in(\mathit{row}(M_{1})\cup\mathit{row}(M_{2}))\times(\mathit{col}(M_{1})\cup\mathit{col}(M_{2}))\leavevmode\nobreak\ M_{1}(r,c)\leq M_{2}(r,c)$; relations $>,\geq,\leq$ are defined analogically. The last operation which we need is matrix multiplication $M_{1}\cdot M_{2}=M_{3}$, it is only allowed if the set of columns of the first matrix $M_{1}$ is the same as the set of rows of the second matrix $M_{2}$, the sets of rows and columns of the resulting matrix $M_{3}$ are rows of the matrix $M_{1}$ and columns of $M_{2}$, respectively. $M_{3}(r,c)=\sum_{k}M_{1}(r,k)M_{2}(k,c)$ where $k$ runs through columns of $M_{1}.$ Again, observe that if the row or a column is equal to [math] for all entries then the effect of multiplication is [math], thus we may restrict to $\mathit{row}(M_{1})$ and $\mathit{col}(M_{2})$. Moreover in the sum it suffices to write $\sum_{k\in\mathit{col}(M_{1})}M_{1}(r,k)M_{2}(k,c).$

3 UDPN, reachability and its variants: Our main results

Unordered data Petri nets extend the classical model of Petri nets by allowing each token to hold a data value from a countably-infinite domain $\mathbb{D}$. Our definition is closest to the definition of $\nu$-Petri Nets from [27]. For simplicity we choose this one instead of using the equivalent but complex one from [18].

Definition 1

Let $\mathbb{D}$ be a countably infinite set. An unordered data Petri net (UDPN) over domain $\mathbb{D}$ is a tuple $(P,T,F,\mathit{Var})$ where $P$ is a finite set of places, $T$ is a finite set of transitions, $\mathit{Var}$ is a finite set of variables, and $F:(P\times T)\cup(T\times P)\to(\mathit{Var}\to\mathbb{N})$ is a flow function that assigns each place $p\in P$ and transition $t\in T$ a function over variables in Var.

For each transition $t\in T$ we define functions {\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}F}(\bullet,t) and {\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}F}(t,\bullet), $\mathit{Var}\to(P\to\mathbb{N})$ as {\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}F}(\bullet,t)(p,x)=F(p,t)(x) and analogously {\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}F}(t,\bullet)(p,x)=F(t,p)(x). Displacement of the transition $t$ is a function $\Delta(t):\mathit{Var}\to(P\to\mathbb{Z})$ defined as $\Delta(t)\overset{\mathrm{def}}{=}F(t,\bullet)-F(\bullet,t)$.

For $\mathbb{X}\in\{\mathbb{N},\mathbb{Z},\mathbb{Q},\mathbb{Q}^{+}\}$, we define an $\mathbb{X}$-marking as a function $M:\mathbb{D}\to(P\to\mathbb{X})$ that is constant [math] on all except finitely many values of $\mathbb{D}$. Intuitively, $M(p,\alpha)$ denotes the number of tokens with the data value $\alpha$ at place $p$. The fact that it is [math] at all but finitely many data means that the number of tokens in any $\mathbb{X}$-marking is finite. We denote the infinite set of all $\mathbb{X}$-markings by $\mathcal{M}_{\mathbb{X}}$.

We define an $\mathbb{X}$-step as a triple $(c,t,\pi)$ for a transition $t\in T$, mode $\pi$ being an injective map $\pi:\mathit{Var}\to\mathbb{D}$, and a scalar constant $c\in\mathbb{X}^{+}$. An $\mathbb{X}$-step $(c,t,\pi)$ is fireable at a $\mathbb{X}$-marking i if ${\textbf{{i}}}-c\cdot F(\bullet,t)\circ\pi^{-1}\in\mathcal{M}_{\mathbb{X}}.$

The $\mathbb{X}$-marking f reached after firing an $\mathbb{X}$-step $(c,t,\pi)$ at i is given as ${\textbf{{f}}}={\textbf{{i}}}+c\cdot\Delta(t)\circ\pi^{-1}$. We also say that an $\mathbb{X}$-step $(c,t,\pi)$ when fired consumes tokens $c\cdot F(\bullet,t)\circ\pi^{-1}$ and produces tokens $c\cdot F(t,\bullet)\circ\pi^{-1}$. We define an $\mathbb{X}$-run as a sequence of $\mathbb{X}$-steps and we can represent it as $\{(c_{i},t_{i},\pi_{i})\}_{|\rho|}$ where $(c_{i},t_{i},\pi_{i})$ is the $i^{th}$ $\mathbb{X}$-step and $|\rho|$ is the number of $\mathbb{X}$-steps. A run $\rho=\{(c_{i},t_{i},\pi_{i})\}_{|\rho|}$ is fireable at a $\mathbb{X}$-marking i if, $\forall 1\leq i\leq|\rho|$, the step $(c_{i},t_{i},\pi_{i})$ is fireable at ${\textbf{{i}}}+\sum_{j=1}^{i-1}c_{i}\Delta(t_{j})\circ\pi_{j}^{-1}$. By ${\textbf{{i}}}\xrightarrow[]{\rho}_{\mathbb{X}}{\textbf{{f}}}$ we denote that $\rho$ is fireable at i and after firing $\rho$ at i we reach $\mathbb{X}$-marking ${\textbf{{f}}}={\textbf{{i}}}+\sum_{i=1}^{|\rho|}c_{i}\cdot\Delta(t_{i})\circ\pi_{i}^{-1}$. We call (the function computed by) the mentioned sum $\sum_{i=1}^{|\rho|}c_{i}\Delta(t_{i})\circ\pi_{i}^{-1}$ as the effect of the run and denote it by $\Delta(\rho)$.

We fix some notations for the rest of the paper. We use Greek letters $\alpha,\beta,\gamma$ to denote data values from data domain $\mathbb{D}$, $\rho$, $\sigma$ to denote a run, $\pi$ to denote a mode and $x,y,z$ to denote the variables. When clear from the context, we may omit $\mathbb{X}$ from $\mathbb{X}$-marking, $\mathbb{X}$-run and just write marking, run, etc. Further, we will use letters in bold, e.g., m to denote markings, where ${\textbf{{i}}},{\textbf{{f}}}$ will be used for initial and final markings respectively. Further, throughout the paper, unless stated explicitly otherwise, we will refer to a UDPN $\mathcal{N}=(P,T,F,\mathit{Var})$, therefore $P,T,F,\mathit{Var}$ will denote the places, transitions, flow, and variables of this UDPN.

Example 1

An example of a simple UDPN $\mathcal{N}_{1}$ is given in Figure 1. For this example, we have $P=\{p_{1},p_{2},p_{3},p_{4}\}$, $T=\{t\}$, $Var=\{x,y,z\}$ and the flow relation is given by $F(p_{1},t)=\{y\mapsto 1\}$, $F(p_{2},t)=\{x\mapsto 1\}$, $F(t,p_{3})=\{y\mapsto 2\}$, $F(t,p_{4})=\{x\mapsto 1,z\mapsto 1\}$, and an assignment of [math] to every variable for the remaining of the pairs. Thus, for enabling transition $p_{1}$ and $p_{2}$ must have one token each with a different data value (since $x\neq y$) and after firing two tokens are produced in $p_{3}$ with same data value as was consumed from $p_{1}$ and two tokens are produced in $p_{4}$, one of whom has same data as consumed from $p_{2}$.

Definition 2

Given $\mathbb{X}$-markings ${\textbf{{i}}},{\textbf{{f}}}$, we say f is $\mathbb{X}$-reachable from i if there exists an $\mathbb{X}$-run $\rho$ s.t., ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{X}}{\textbf{{f}}}$.

When $\mathbb{X}=\mathbb{N}$, $\mathbb{X}$-reachability is the classical reachability problem, whose decidability is still unknown, while $\mathbb{Z}$-reachability for UDPN is in NP [22].

In this paper we tackle $\mathbb{Q}$ and $\mathbb{Q}^{+}$-reachability, also called continuous reachability in UDPN.

The first step towards the solution is showing that if a $\mathbb{Q}^{+}$-marking f is $\mathbb{Q}^{+}$-reachable from a $\mathbb{Q}^{+}$-marking i, then there exists a $\mathbb{Q}^{+}$-run $\rho$ which uses polynomially many data values and ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{Q}^{+}}{\textbf{{f}}}$. We first formalize the set of distinct data values associated with $\mathbb{X}$-markings, data values used in $\mathbb{X}$-runs and variables associated with a transition.

Definition 3

For $\mathcal{N}=(P,T,F,\mathit{Var})$ a UDPN, $\mathbb{X}$-marking m, $t\in T$, and $\mathbb{X}$-run $\rho=\{(c_{i},t_{i},\pi_{i})\}_{|\rho|}$, we define

$\mathit{dval}(\textbf{{m}})=\{\alpha\in\mathbb{D}\mid\leavevmode\nobreak\ \exists p\in P:\textbf{{m}}(p,\alpha)\neq 0\}$. 2. 2.

$\mathit{dval}(\rho)=\{\alpha\in\mathbb{D}\mid\leavevmode\nobreak\ \exists i\leq|\rho|\leavevmode\nobreak\ \exists x\in\mathit{dval}(t_{i}):(\pi_{i}(x)=\alpha)\}$. 3. 3.

$\mathit{vars}(t)=\{x\in\mathit{Var}\mid\leavevmode\nobreak\ \exists p\in P\leavevmode\nobreak\ :F(p,t)(x)\neq 0\lor F(t,p)(x)\neq 0\}$.

With this we state the first main result of this paper, which provides a bound on witnesses of $\mathbb{Q},\mathbb{Q}^{+}$-reachability, and is proved in Section 5.

Theorem 3.1

For $\mathbb{X}\in\{\mathbb{Q},\mathbb{Q}^{+}\}$, if an $\mathbb{X}$-marking f is $\mathbb{X}$-reachable from an initial $\mathbb{X}$-marking i, then there is an $\mathbb{X}$-run $\rho$ such that ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{X}}{\textbf{{f}}}$ and $|\mathit{dval}(\rho)|\leq|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})|+1+\max_{t\in T}(|\mathit{vars}(t)|)$.

Using the above bound, we obtain a polynomial time algorithm for $\mathbb{Q}$-reachability, as detailed in Section 6.

Theorem 3.2 ()

Given $\mathcal{N}=(P,T,F,\mathit{Var})$ a UDPN and two $\mathbb{Q}$-markings i, f, deciding if f is $\mathbb{Q}$-reachable from i in $\mathcal{N}$ is in polynomial time.

Finally, we consider continuous, i.e., $\mathbb{Q}^{+}$-reachability for UDPN. We adapt the techniques used for $\mathbb{Q}^{+}$-reachability of Petri nets without data from [11, 12] to the setting with data, and obtain a characterization of $\mathbb{Q}^{+}$-reachability for UDPN in Section 7.1. Finally, in Section 7.3, we show how the characterization can be combined with the above bound and compression techniques from [22] to obtain a polynomial sized system of linear equations with implications over $\mathbb{Q}^{+}$. To do so, we require a slight transformation of the net which is described in Section 7.2.

This leads to our headline result, stated below.

Theorem 3.3 (Continuous reachability for UDPN)

Given $\mathcal{N}=(P,T,F,\mathit{Var})$ a UDPN and two $\mathbb{Q}^{+}$-markings i, f, deciding if f is $\mathbb{Q}^{+}$-reachable from i in $\mathcal{N}$ is in polynomial time.

The rest of this paper is dedicated to proving these theorems. First, we present an equivalent formulation via matrices, which simplifies the technical arguments.

4 Equivalent formulation via Matrices

From now on, we restrict $\mathbb{X}$ to a symbol denoting $\mathbb{Q}$ or $\mathbb{Q}^{+}.$ We formulate the definitions presented earlier in terms of matrices, since defining object such as $\mathbb{X}$-marking as functions is intuitive to define but difficult to operate upon.

In the following, we abuse the notation and use the same names for objects as well as matrices representing them. We remark that this is safe as all arithmetic operations on objects correspond to matching operations on matrices.

An $\mathbb{X}$-marking m is a $P\times\mathbb{D}$ matrix $M$, where $\forall p\in P,\forall\alpha\in\mathbb{D},M(p,\alpha)=\textbf{{m}}(p,\alpha)$. As a finite representation, we keep only a $P\times\mathit{dval}(\textbf{{m}})$ matrix of non-zero columns. For a transition $t\in T$, we represent $F(t,\bullet),F(\bullet,t)$ as $P\times\mathit{Var}$ matrices. Note that $(t,\bullet)$ is not the position in the matrix, but is part of the name of the matrix; its entry at $(i,j)\in P\times\mathit{Var}$ is given by $F(t,\bullet)(i,j)$. For a place $p\in\mathit{row}(F(t,\bullet))$, the row $F(t,\bullet)(p,\bullet)$ is a vector in $\mathbb{N}^{\mathit{Var}}$, given by an equation $F(\bullet,t)(p,\bullet)(x)=F(p,t)(x)$ for $p\in P,t\in T,x\in\mathit{Var}.$ Similarly, $\Delta(t)$ is a $P\times\mathit{Var}$ matrix with $\Delta(t)(p,x)=F(t,\bullet)(p,x)-F(\bullet,t)(p,x)$ for $t\in T,p\in P,\text{ and }x\in\mathit{Var}.$ Although, both $\Delta(t)$ and $F(\bullet,t)$ are defined as $P\times\mathit{Var}$ matrices, only the columns for variables in $\mathit{vars}(t)$ may be non-zero, so often we will iterate only over $\mathit{vars}(t)$ instead of $\mathit{Var}$.

Finally, we capture a mode $\pi:\mathit{Var}\to\mathbb{D}$ as a $\mathit{Var}\times\mathbb{D}$ permutation matrix ${\mathcal{P}}$. Although ${\mathcal{P}}$ may not be a square matrix, we abuse notation and call them permutation matrices. ${\mathcal{P}}$ basically represents assignment of variables in $\mathit{Var}$ to data values just like $\pi$ does. An entry of 1 represents that the corresponding variable is assigned corresponding data value in mode $\pi$. Thus, for each mode $\pi:\mathit{Var}\to\mathbb{D}$ there is a permutation matrix ${\mathcal{P}}_{\pi}$, such that for all $x\in\mathit{Var}$, $\alpha\in\mathit{col}({\mathcal{P}}_{\pi})$, ${\mathcal{P}}_{\pi}(x,\alpha)=1$ if $\pi(x)=\alpha$, and ${\mathcal{P}}_{\pi}(x,\alpha)=0$ otherwise. Formulating a mode as a permutation matrix has the advantage that $\Delta(t)\circ\pi^{-1}$ is captured by $\Delta(t)\cdot{\mathcal{P}}_{\pi}$ where ${\mathcal{P}}_{\pi}$ can be represented as a sub-matrix of actual ${\mathcal{P}}_{\pi}$, whose set of row indices is limited to the set of column indices of the matrix $\Delta(t)$.

Example 2

In the UDPN $\mathcal{N}_{1}$ from Example 1, the initial marking i can be represented by the matrix i below and the function $\Delta(t)$ by the matrix $\Delta(t)$

[TABLE]

If we fire transition $t$ with the assignment $x=blue,y=green,z=black$, we get the following net depicted below (left), with marking f (below center). The permutation matrix corresponding to the mode of fired transition is given by ${\mathcal{P}}$ matrix on the right. Note that the matrix ${\textbf{{f}}}-{\textbf{{i}}}$ is indeed the matrix $\Delta(t)\cdot{\mathcal{P}}$.

[TABLE]

Using the representations developed so far we can represent an $\mathbb{X}$-run $\rho$ as $\{(c_{i},t_{i},{\mathcal{P}}_{i})\}_{|\rho|}$ where $(c_{i},t_{i},{\mathcal{P}}_{i})$ denotes the $i^{th}$ $\mathbb{X}$-step fired with coefficient $c_{i}$ using transition $t_{i}$ with a mode corresponding to the permutation matrix ${\mathcal{P}}_{i}$. The sum of the matrices ($\sum_{i=1}^{|\rho|}c_{i}\Delta(t_{i})\cdot{\mathcal{P}}_{i}$) gives us the effect of the run i.e. $\Delta(\rho)={\textbf{{f}}}-{\textbf{{i}}}$ where ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{X}}{\textbf{{f}}}$. Effect of an $\mathbb{X}$-run $\rho$ on a data value $\alpha$ is $\Delta(\rho)(\bullet,\alpha)$. Also, for an $\mathbb{X}$-run $\rho=\{(c_{i},t_{i},{\mathcal{P}}_{i})\}_{|\rho|}$ , define $k{\rho}=\{(k{c_{i}},t_{i},{\mathcal{P}}_{i})\}_{|\rho|}$ where $k\in\mathbb{X}^{+}$.

5 Bounding number of data values used in ${\mathbb{Q},\mathbb{Q}^{+}}$-run

We now prove the first main result of the paper, namely, Theorem 3.1, which shows a linear upper bound on the number of data values required in a $\mathbb{Q}^{+}$-run and a $\mathbb{Q}$-run. Theorem 3.1 is an immediate consequence of the following lemma, which states that if more than a linearly bounded number of data values are used in a $\mathbb{Q}$ or $\mathbb{Q}^{+}$ run, then there is another such run in which we use at least one less data value.

Lemma 1

Let $\mathbb{X}\in\{\mathbb{Q},\mathbb{Q}^{+}\}$. If there exists an $\mathbb{X}$-run $\sigma$ such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{X}}{\textbf{{f}}}$ and $|\mathit{dval}(\sigma)|>|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})|+1+\max_{t\in T}(|\mathit{vars}(t)|)$, then there exists an $\mathbb{X}$-run $\rho$ such that ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{X}}{\textbf{{f}}}$ and $|\mathit{dval}(\rho)|\leq|\mathit{dval}(\sigma)|-1$.

By repeatedly applying this lemma, Theorem 3.1 follows immediately. The rest of this section is devoted to proving this lemma. The central idea is to take any $\mathbb{Q}$ or $\mathbb{Q}^{+}$-run between i, f and transform it to use at least one data value less.

5.1 Transformation of an $\mathbb{X}$-run

The transformation which we call decrease is defined as a combination of two separate operations on an $\mathbb{X}$-run; we name them $\mathit{uniformize}$ and $\mathit{replace}$ and denote them by $\mathcal{U}$ and $\mathcal{R}$ respectively.

• •

$\mathit{uniformize}$ takes an $\mathbb{X}$-step and a non-empty 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.

• •

$\mathit{replace}$ takes an $\mathbb{X}$-step, a single data value $\alpha,$ and a non-empty set of data values ${\mathbb{E}}$ as input and outputs an $\mathbb{X}$-step which doesn’t use data value $\alpha$.

The intuition behind the decrease operation is that we would like to take two data values $\alpha$ and $\beta$ used in the run such that effect on both of them is 0 (they exists as the effect on every data value not present in the initial of final configuration is 0) and replace usage of $\alpha$ by $\beta$. However, such a replacement can only be done if both data are not used together in a single step (indeed, a mode $\pi$ cannot assign the same data values to two variables). Unfortunately we cannot guarantee the existence of such a $\beta$ that may replace $\alpha$ globally. We circumvent this by applying the $\mathit{replace}$ operation separately for every step, replacing $\alpha$ with different data values in different steps.

But such a transformation would not preserve the effect of the run. To repair this aspect we uniformize i.e. guarantee that the final effect after replacing $\alpha$ by other data values is equal for every datum that is used to replace $\alpha$. As the effect on $\alpha$ was 0 then if we split it uniformly it adds 0 to effects of data replacing $\alpha$, which is exactly what we want. We now formalize this intuition below.

5.1.1 The uniformize operator.

By $\copyright$ we denote an operator of concatenation of two sequences. Although the data set $\mathbb{D}$ is unordered, the following definitions require access to an arbitrary but fixed linear order on its elements. The definition of the $\mathit{uniformize}$ operator needs another operator to act on an $\mathbb{X}$-step, which we call $\mathit{rotate}$ and denote by $\mathit{rot}$.

Definition 4

For a non-empty set of data values ${\mathbb{E}}\subset\mathbb{D}$ and an $\mathbb{X}$-step, $\omega=(c,t,{\mathcal{P}})$, define $\mathit{rot}({\mathbb{E}},\omega)=(c,t,{\mathcal{P}}^{\prime})$ where ${\mathcal{P}}^{\prime}$ is obtained from ${\mathcal{P}}$ as follows.

• •

$\forall\alpha\in\mathit{col}({\mathcal{P}})\setminus{\mathbb{E}}$, ${\mathcal{P}}^{\prime}(\bullet,\alpha)={\mathcal{P}}(\bullet,\alpha)$.

• •

$\forall\alpha\in{\mathbb{E}}$, ${\mathcal{P}}^{\prime}(\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.

For a fixed set ${\mathbb{E}}$, we can repeatedly apply $\mathit{rot}({\mathbb{E}},\bullet)$ operation on an $\mathbb{X}$-step, which we denote by $\mathit{rot}^{k}({\mathbb{E}},\omega)$, where $k$ is the number of times we applied the operation (for example: $\mathit{rot}^{2}({\mathbb{E}},\omega)=\mathit{rot}({\mathbb{E}},(\mathit{rot}({\mathbb{E}},\omega))$).

Definition 5

For a non-empty set of data values ${\mathbb{E}}\subset\mathbb{D}$ and an $\mathbb{X}$-step $\omega=(c,t,{\mathcal{P}})$, we define $\mathit{uniformize}$ as follows

$\mathcal{U}({\mathbb{E}},\omega)=\mathit{rot}^{0}({\mathbb{E}},\frac{\omega}{|{\mathbb{E}}|})\leavevmode\nobreak\ \copyright\leavevmode\nobreak\ \mathit{rot}^{1}({\mathbb{E}},\frac{\omega}{|{\mathbb{E}}|})\leavevmode\nobreak\ \copyright\leavevmode\nobreak\ \mathit{rot}^{2}({\mathbb{E}},\frac{\omega}{|{\mathbb{E}}|})\leavevmode\nobreak\ \copyright\leavevmode\nobreak\ ...\leavevmode\nobreak\ \copyright\leavevmode\nobreak\ \mathit{rot}^{|{\mathbb{E}}|-1}({\mathbb{E}},\frac{\omega}{|{\mathbb{E}}|})$.

An important property of uniformize is its effect on data values.

Lemma 2 ()

For a non-empty set of data values ${{\mathbb{E}}}\subset\mathbb{D}$ and an $\mathbb{X}$-step $\omega=(c,t,{\mathcal{P}})$, ${\textbf{{i}}}\xrightarrow{\omega}_{\mathbb{Q}^{+}}{\textbf{{f}}}$, if ${\textbf{{i}}}^{\prime}\xrightarrow{\mathcal{U}({{\mathbb{E}}},\omega)}{\textbf{{f}}}^{\prime}$, then

$\forall\alpha\in\mathit{dval}(\omega)\backslash{{\mathbb{E}}}$, ${\textbf{{f}}}^{\prime}(\bullet,\alpha)-{\textbf{{i}}}^{\prime}(\bullet,\alpha)={\textbf{{f}}}(\bullet,\alpha)-{\textbf{{i}}}(\bullet,\alpha)$ 2. 2.

$\forall\alpha\in{{\mathbb{E}}},\leavevmode\nobreak\ ,{\textbf{{f}}}^{\prime}(\bullet,\alpha)-{\textbf{{i}}}^{\prime}(\bullet,\alpha)=\frac{\sum_{\beta\in{{\mathbb{E}}}}({\textbf{{f}}}(\bullet,\beta)-{\textbf{{i}}}(\bullet,\beta))}{|{\mathbb{E}}|}$.

This lemma tells us the effect of the run on the initial marking is equalized for data values in ${{\mathbb{E}}}$ by the $\mathcal{U}$ operation, and is unchanged for the other data values.

5.1.2 The replace operator.

To define the $\mathit{replace}$ operator it is useful to introduce $swap_{\alpha,\beta}({\mathcal{P}})$ which exchanges columns $\alpha$ and $\beta$ in the matrix ${\mathcal{P}}$.

Definition 6

For a set of data values ${\mathbb{E}}$, an $\mathbb{X}$-step $\omega=(c,t,{\mathcal{P}})$, and $\alpha\not\in{\mathbb{E}}$ we define $\mathit{replace}$ as follows

[TABLE]

After applying the $\mathit{replace}$ operation $\alpha$ is no longer used in the run, which reduces the number of data values used in the run. Observe that $\mathit{replace}$ can not be always applied to an $\mathbb{X}$-step. It requires a zero column labelled with an element from ${\mathbb{E}}$ in the permutation matrix corresponding to the $\mathbb{X}$-step.

5.1.3 The decrease transformation.

Now we are ready to define the final transformation on an $\mathbb{X}$-run between two markings which we call $\mathit{decrease}$ and denote by $\mathit{dec}$.

Definition 7

For two $\mathbb{X}$-markings i, f, and an $\mathbb{X}$-run $\sigma$ such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{X}}{\textbf{{f}}}$ and $|\mathit{dval}(\sigma)|>|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})|+1+\max_{t\in T}(|\mathit{vars}(t)|)$, let $\{\alpha\}\cup{\mathbb{E}}=\mathit{dval}(\sigma)\setminus(\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}}))$ and $\alpha\not\in{\mathbb{E}}$. We define $\mathit{decrease}$ by, $\mathit{dec}({\mathbb{E}},\alpha,\sigma)=$

[TABLE]

where $\sigma(j)$ denotes the $j^{th}$ $\mathbb{X}$-step of $\sigma$.

Observe that the required size of $\mathit{dval}(\sigma)$ guarantees existence of a $\beta\in{\mathbb{E}}$ which can be replaced with $\alpha$, for every application of the $\mathcal{R}$ operation. Note that the exchanged data value $\beta$ could be different for each step. Finally, we can analyze the $\mathit{decrease}$ transformation and show that if the original run allows for the $\mathit{decrease}$ transformation (as given in the above definition), then after the application of it, the resulting sequence of transitions is a valid run of the system.

Lemma 3

Let $\sigma$ be an $\mathbb{X}$-run such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{X}}{\textbf{{f}}}$ and $|\mathit{dval}(\sigma)|>|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})|+1+\max_{t\in T}(|\mathit{dval}(t)|)$. Let $\alpha\in\mathit{dval}(\sigma)\setminus(\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}}))$ and ${\mathbb{E}}=\mathit{dval}(\sigma)\setminus(\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})\cup\{\alpha\})$. Then for $\rho=\mathit{dec}({\mathbb{E}},\alpha,\sigma)$, we obtain ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{X}}{\textbf{{f}}}.$

Proof

Suppose $\sigma=\sigma_{1}\sigma_{2}\ldots\sigma_{l}$ where each $\sigma_{j}=(c_{j},t_{j},{\mathcal{P}}_{j})$, for $1\leq j\leq l$ is an $\mathbb{X}$-step. Then $\rho=\rho_{1}\copyright\ldots\copyright\rho_{l}$, where each $\rho_{j}$ is an $\mathbb{X}$-run defined by $\rho_{j}=\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))$. It will be useful to identify intermediate $\mathbb{X}$-markings

[TABLE]

We split the proof: first we show that ${\textbf{{f}}}={\textbf{{f}}}^{\prime}$ and then $\rho$ is $\mathbb{X}$-fireable from ${\textbf{{i}}}.$

Step 1: Showing that the final markings reached are the same. We prove a stronger statement which implies that ${\textbf{{f}}}={\textbf{{f}}}^{\prime}$, namely:

Claim 1 ()

For all $0\leq j\leq l$

$\textbf{{m}}_{j}^{\prime}(\bullet,\alpha)=\textbf{0}$** 2. 2.

$\forall\gamma\in$* $\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})$, $\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)=\textbf{{m}}_{j}(\bullet,\gamma)$* 3. 3.

$\forall\gamma\in$* ${{\mathbb{E}}}$ $\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)=\frac{1}{|{\mathbb{E}}|}\left(\sum_{\delta\in{{\mathbb{E}}}\cup\{\alpha\}}\textbf{{m}}_{j}(\bullet,\delta)\right).$*

The proof is obtained by induction on $j$, and is a resulting computations as detailed in Appendix 9.1. Intuitively, point 1 holds as we shift effects on $\alpha$ to $\beta$-s, point 2 holds as the transformation does not touch $\gamma\in\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}}).$ The last most complicated point follows from the fact that the number of tokens consumed and produced along each $\xrightarrow{\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))}$ is the same as for $\sigma_{j}$, but uniformized over ${\mathbb{E}}$.

Step 2: Showing that $\rho$ is an $\mathbb{X}$-run. If $\mathbb{X}=\mathbb{Q}$ then the run $\rho$ is fireable, as any $\mathbb{Q}$-run is fireable, so in this case this step is trivial. The case when $\mathbb{X}=\mathbb{Q}^{+}$ is more involved. As we know from claim 1 , each $m_{j}^{\prime}$ is a $\mathbb{Q}^{+}$-marking, so it suffices to prove that for every $j$, $\textbf{{m}}_{j}^{\prime}\xrightarrow{\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))}_{\mathbb{Q}^{+}}\textbf{{m}}_{j+1}^{\prime}$. Consider a data vector of tokens consumed along the $\mathbb{Q}^{+}$-run $\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))$. If we show that it is smaller than or equal to $\textbf{{m}}_{j}^{\prime}$ (component-wise), then we can conclude that $\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))$ is indeed $\mathbb{Q}^{+}$-fireable from $\textbf{{m}}_{j}^{\prime}$. To show this, we examine the consumed tokens for each datum $\gamma$ separately. There are three cases:

• (i)

$\gamma=\alpha$. For this case, every step in $\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))$ does not make any change on $\alpha$ so tokens with data value $\alpha$ are not consumed along the $\mathbb{Q}^{+}$-run $\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))$.

• (ii)

$\gamma\in\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})$. This is similar to the above case. Consider any data value $\gamma\in(\mathit{dval}(\sigma)\backslash{{\mathbb{E}}})\setminus\{\alpha\}$. Since $\gamma$ does not change on $\mathit{rotate}$ operation, the $\mathcal{U}$ operation causes each $\mathbb{Q}$-step in $\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))$ to consume $\frac{1}{|{\mathbb{E}}|}$ of the tokens with data value $\gamma$ consumed when $\sigma_{j}$ is fired. This is repeated $|{\mathbb{E}}|$ times and hence the vector of tokens with data value $\gamma$ consumed along $\mathcal{U}({{\mathbb{E}}},\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j}))$ is equal to the vector of tokens with value $\gamma$ consumed by step $\sigma_{j}$. But we know that, it is smaller than $\textbf{{m}}_{j}(\bullet,\gamma)$ and concluding smaller than $\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)$. The last inequality is true as $\textbf{{m}}_{j}(\bullet,\gamma)=\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)$ according to Claim 1.

• (iii)

$\gamma\in{\mathbb{E}}$. Let $\omega$ be a triple $(c_{j},F(\bullet,t_{j}),{\mathcal{P}}_{j})$ where $(c_{j},t_{j},{\mathcal{P}}_{j})=\sigma_{j}.$ $\omega$ simply describes tokens consumed by $\sigma_{j}.$ We slightly overload the notation and treat a triple $\omega$ like a step, where $F(\bullet,t_{j})$ represents a transition ”_” for which $F(\bullet,\_)=F(\bullet,t_{j})$ and $F(\_,\bullet)$ is a zero matrix. We calculate the vector of consumed tokens with data value $\gamma$ as follows: $consumed(\bullet,\gamma)=$

[TABLE]

the first equality is from definition and the second by the $\mathit{replace}$ operation,

[TABLE]

Further, observe that as $\sigma_{j}$ can fired in $\textbf{{m}}_{j}$

[TABLE]

summing up over $\delta\in{\mathbb{E}}\cup\{\alpha\}$ and multiplying with $\frac{1}{|{\mathbb{E}}|}$ we get

[TABLE]

where the last equality comes from Claim 1 point 3. Combining inequalities we get $consumed(\bullet,\gamma)\leq\textbf{{m}}_{i}^{\prime}(\bullet,\gamma)$.

Proof (of Lemma 1)

Now the proof of Lemma 1 (and hence Theorem 3.1) follow immediately, since we can use the $\mathit{decrease}$ transformation, to decrease the number of data values required in an $\mathbb{X}$-run. We simply take $\alpha\in\mathit{dval}(\sigma)\setminus(\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}}))$ and ${\mathbb{E}}=\mathit{dval}(\sigma)\setminus(\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}}))\setminus\{\alpha\}.$ Next, let $\rho=\mathit{dec}({{\mathbb{E}}},\alpha,\sigma)).$ Due to Lemma 3 we know that ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{X}}{\textbf{{f}}}$. Moreover, observe that $\mathit{dval}(\rho)\subseteq\mathit{dval}(\sigma)$. But in addition, $\alpha\not\in\mathit{dval}(\rho)$ as due to the one of properties of the $\mathit{decrease}$ operation $\alpha$ does not participate in the run $\rho$. So $\mathit{dval}(\rho)\subset\mathit{dval}(\sigma).$ Therefore $|\mathit{dval}(\rho)|\leq|\mathit{dval}(\sigma)|-1$.

6 $\mathbb{Q}$-reachability is in PTime

We recall the definition of histograms from [22].

Definition 8

A histogram $M$ of order $q\in\mathbb{Q}$ is a $\mathit{Var}\times\mathbb{D}$ matrix having non-negative rational entries such that,

$\sum_{\alpha\in\mathit{col}(M)}M(x,\alpha)=q$ for all $x\in\mathit{row}(M)$. 2. 2.

$\sum_{x\in\mathit{row}(M)}M(x,\alpha)\leq q$ for all $\alpha\in\mathit{col}(M)$.

A permutation matrix is a histogram of order 1.

We now state two properties of histograms in the following lemma. We say that a histogram of order $a$ is an [$a$]-histogram if the histogram has only $\{0,a\}$ entries.

Lemma 4 ()

Let $H,H_{1},H_{2},..,H_{n}$ be histograms of order $q,q_{1},q_{2},...,q_{n}$ respectively and of same row dimensions then (i) $\sum_{i=1}^{n}H_{i}$ is a histogram of order $\sum_{i}^{n}q_{i}$, (ii) $H$ can be decomposed as a sum of [$a_{i}$]-histograms such that $\sum_{i}a_{i}=q$.

Using histograms we define a representation $Hist(\rho)$ for an $\mathbb{X}$-run $\rho$, which captures $\Delta(\rho)$. From an $\mathbb{X}$-run $\rho=\{(c_{j},t_{j},{\mathcal{P}}_{j})\}_{|\rho|}$ we obtain $Hist(\rho)$ as follows. For all transitions $t\in T$, define the set $I_{t}=\{j\in[1..|\rho|]|\leavevmode\nobreak\ t_{j}=t\}$. Then calculate the matrix $H_{t}=\sum_{i\in I_{t}}c_{i}{\mathcal{P}}_{i}$. Observe that since permutation matrices are histograms and histograms are closed under scalar multiplication and addition, $H_{t}$ is a histogram. If $I_{t}$ is empty, then $H_{t}$ is simply the null matrix. We define $Hist(\rho)$ as a mapping from $T$ to histograms such that $t$ is mapped to $H_{t}$.

Analogous to an $\mathbb{X}$-run we can represent $Hist(\rho)$ simply as $\{(t_{j},H_{t_{j}})\}$, unlike an $\mathbb{X}$-run we don’t indicate the length of the sequence since it is dependent on the net and not the individual run itself.

Proposition 1

Let $\mathcal{N}=(P,T,F,\mathit{Var})$ be a UDPN, ${\textbf{{i}}},{\textbf{{f}}}$  $\mathbb{X}$-markings, and $\sigma$ an $\mathbb{X}$-run such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{X}}{\textbf{{f}}}$. Then for each $t\in T$ there exists $H_{t}$ such that:

${\textbf{{f}}}-{\textbf{{i}}}=\sum_{t\in T}\Delta(t)\cdot H_{t},$** 2. 2.

$\mathit{col}(H_{t})\subseteq\mathit{dval}(\sigma)$* for every $t\in T.$*

A PTime Procedure. We start by observing that from any $\mathbb{Q}$-marking i, every $\mathbb{Q}$-step $(c,t,{\mathcal{P}})$ is fireable and every $\mathbb{Q}$ run is fireable. This follows from the fact that rationals are closed under addition, thus ${\textbf{{i}}}+c\cdot F(\bullet,t)\cdot{\mathcal{P}}$ is a marking in $\mathcal{M}_{\mathbb{Q}}$. Thus if we have to find a $\mathbb{Q}$-run $\rho=\{(c_{j},t_{j},{\mathcal{P}}_{j})\}_{|\rho|}$ between two $\mathbb{Q}$-markings, ${\textbf{{i}}},{\textbf{{f}}}$ it is sufficient to ensure that ${\textbf{{f}}}-{\textbf{{i}}}=\sum_{j=1}^{|\rho|}c_{j}\Delta(t_{j})\cdot{\mathcal{P}}_{j}$. Thus for a $\mathbb{Q}$-run all that matters is the difference in markings caused by the $\mathbb{Q}$-run which is captured succinctly by $Hist(\rho)=\{t_{j},H_{t_{j}}\}$. This brings us to our characterization of $\mathbb{Q}$-run.

Lemma 5 ()

Let $\mathcal{N}=(P,T,F,\mathit{Var})$ be a UDPN, a marking f is $\mathbb{Q}$-reachable from i iff there exists set ${\mathbb{E}}$ of size bounded by $|{\mathbb{E}}|\leq|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})|+1+\max_{t\in T}(|\mathit{vars}(t)|)$ and a histogram $H_{t}$ for each $t\in T$ such that ${\textbf{{f}}}-{\textbf{{i}}}=\sum_{t\in T}\Delta(t)\cdot H_{t}$ and $\forall t\in T\leavevmode\nobreak\ \mathit{col}(H_{t})\subseteq{\mathbb{E}}.$

Using this characterization we can write a system of linear inequalities to encode the condition of Lemma 5. Thus, we obtain our second main result, with detailed proofs in the Appendix 9.2. See 3.2

7 $\mathbb{Q}^{+}$-reachability is in PTime

Finally, we turn to $\mathbb{Q}^{+}$-reachability for UDPNs and to the proof of Theorem 3.3. At a high level, the proof is in three steps. We start with a characterization of $\mathbb{Q}^{+}$-reachability in UDPNs.

Then we present a polytime reduction of the continuous reachability problem to the same problem but for a special subclass of UDPN, called loop-less nets. Finally, we present how to encode the characterization for loop-less nets into a system of linear equations with implications to obtain a polytime algorithm for continuous reachability in UDPNs.

7.1 Characterizing $\mathbb{Q}^{+}$-reachability

We begin with a definition. For an $\mathbb{X}$-run we introduce the notion of the pre and post sets of $\mathbb{X}-$run. For an $\mathbb{X}$-run, $\rho=\{(c_{i},t_{i},{\mathcal{P}}_{i})\}_{|\rho|}$ we define $Pre(\rho)=\{(\alpha,p)|\leavevmode\nobreak\ \exists\leavevmode\nobreak\ t_{i},\exists\leavevmode\nobreak\ x:F(p,t_{i})(x)<0\wedge{\mathcal{P}}_{i}(x,\alpha)=1\}$. We also define $Post(\rho)=\{(\alpha,p)|\leavevmode\nobreak\ \exists\leavevmode\nobreak\ t_{i},\exists\leavevmode\nobreak\ x:F(t_{i},p)(x)>0\wedge{\mathcal{P}}_{i}(x,\alpha)=1\}$. Intuitively, $Pre(\rho)/Post(\rho)$ denote the set of $(\alpha,p)$ (data value,place) pairs describing tokens that are consumed/produced by the run $\rho$.

Throughout this section, by a marking we denote a $\mathbb{Q}^{+}$-marking.

Lemma 6 ()

Let $\mathcal{N}=(P,T,F,\mathit{Var})$ be an UDPN and ${\textbf{{i}}},{\textbf{{f}}}$ are markings. For any $\mathbb{Q}^{+}$-run $\sigma$ such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{Q}^{+}}{\textbf{{f}}}$ there exist markings ${\textbf{{i}}}^{\prime}$ and ${\textbf{{f}}}^{\prime}$ (possibly on a different run) such that

${\textbf{{i}}}^{\prime}$* is $\mathbb{Q}^{+}$-reachable from i in at most $|P|\cdot|\mathit{dval}(\sigma)|$ $\ \mathbb{Q}^{+}$-steps* 2. 2.

There is a run $\sigma^{\prime}$ such that $\mathit{dval}(\sigma^{\prime})\subseteq\mathit{dval}(\sigma)$ and ${\textbf{{i}}}^{\prime}\xrightarrow{\sigma^{\prime}}_{\mathbb{Q}}{\textbf{{f}}}^{\prime}$ 3. 3.

f* is $\mathbb{Q}^{+}$-reachable from ${\textbf{{f}}}^{\prime}$ in at most $|P|\cdot|\mathit{dval}(\sigma)|$    $\mathbb{Q}^{+}$-steps* 4. 4.

$\forall(p,\alpha)\in Pre(\sigma^{\prime}),{\textbf{{i}}}^{\prime}(p,\alpha)>0$** 5. 5.

$\forall(p,\alpha)\in Post(\sigma^{\prime}),{\textbf{{f}}}^{\prime}(p,\alpha)>0$**

Remark 1 ()

If in conditions 1 and 3 we drop the requirement on the number of steps then the five conditions still imply continuous reachability.

Note that if there exist markings ${\textbf{{i}}}^{\prime}$ and ${\textbf{{f}}}^{\prime}$ and $\mathbb{Q}^{+}$ runs $\rho$, $\rho^{\prime}$, $\rho^{\prime\prime}$ such that ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{Q}^{+}}{\textbf{{i}}}^{\prime},{\textbf{{i}}}^{\prime}\xrightarrow{\rho^{\prime}}_{\mathbb{Q}^{+}}{\textbf{{f}}}^{\prime},{\textbf{{f}}}^{\prime}\xrightarrow{\rho^{\prime\prime}}_{\mathbb{Q}^{+}}{\textbf{{f}}}$ then there is a $\mathbb{Q}^{+}$ run $\sigma$ such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{Q}^{+}}{\textbf{{f}}}$.The above characterization and its proof are obtained by adapting to the data setting, the techniques developed for continuous reachability in Petri nets (without data) in [11] and  [12]. Details are in Appendix 9.3.

7.2 Transforming UDPN to loop-less UDPN

For a UDPN $\mathcal{N}=(P,T,F,\mathit{Var})$, we construct a UDPN $N^{\prime}$ which is polynomial in the size of $N$ and for which the $\mathbb{Q}^{+}$-reachabilty problem is equivalent.

We define $PrePlace(t)=\{p\in P|\exists v\in\mathit{Var}\ s.t.\ F(p,t)(v)>0\}$ and $PostPlace(t)=\{p\in P|\exists v\in\mathit{Var}\ s.t.\ F(t,p)(v)>0\}$, where $t\in T$. The essential property of the transformed UDPN is that for every transition the sets of PrePlace and PostPlace do not intersect. A UDPN $N=(P,T,F,\mathit{Var})$ is said to be loop-less if for all $t\in T$, $PrePlace(t)\cap PostPlace(t)=\emptyset.$

Any UDPN can easily be transformed in polynomial time into a loop-less UDPN such that $\mathbb{Q}^{+}$-reachability is preserved, by doubling the number of places and adding intermediate transitions. Formally, For every net $N$ and two markings ${\textbf{{i}}},{\textbf{{f}}}$ in polynomial time one can construct a loop-less net $N^{\prime}$ and two markings ${\textbf{{i}}}^{\prime},\ {\textbf{{f}}}^{\prime}$ such that ${\textbf{{i}}}\xrightarrow{}_{\mathbb{Q}^{+}}{\textbf{{f}}}$ in the net $N$ iff ${\textbf{{i}}}^{\prime}\xrightarrow{}_{\mathbb{Q}^{+}}{\textbf{{f}}}^{\prime}$ in $N^{\prime}.$ The proof of this statement is formalized in Section 9.4 in the Appendix, along with examples and transformation. Now, the following lemma which describes a property of loop-less nets will be crucial for our reachability algorithm:

Lemma 7 ()

In a loop-less net, for markings i, f, if there exist a histogram $H$, and a transition t $\in$ T such that ${\textbf{{i}}}+\Delta(t)\cdot H={\textbf{{f}}}$, then there exist a $\mathbb{Q}^{+}$-run $\rho$ such that ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{Q}^{+}}{\textbf{{f}}}$.

7.3 Encoding $\mathbb{Q}^{+}$-reachability as linear equations with implications

Linear equations with implications are defined exactly as we use it in [23] but they were introduced in [12]. We also call a system of linear equations with implications a $\implies$ system. A $\implies$ -system is a finite set of linear inequalities, all over the same variables, plus a finite set of implications of the form $x>0\implies y>0$, where $x,y$ are variables appearing in the linear inequalities.

Lemma 8

[12]** The $\mathbb{Q}^{+}$ solvability problem for a $\implies$ system is in $PTime$.

Our aim here will be to reduce the $\mathbb{Q}^{+}$-reachability problem to checking the solvability of a system of linear equations with implications, using the characterization of the problem established in Lemma 6.

Lemma 9

$\mathbb{Q}^{+}$-reachability in a UDPN $N=(P,T,F,\mathit{Var})$ between markings ${\textbf{{i}}},{\textbf{{f}}}$ can be encoded as a set of linear equations with implications in P-time.

Proof

As mentioned in Subsection 7.2 , without loss of generality we may assume that UDPN $N$ is loop-less. Invoking Theorem 3.1 w.l.o.g we can assume that the $\mathbb{Q}^{+}$-run $\sigma$ uses at most $|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{i}}})|+1+\max_{t\in T}(|\mathit{vars}(t)|)$ data values, call $\mathbb{Y}$ the set of data vales used by $\sigma$.

As we need to describe several linear constraints we present them in terms of matrix multiplication. We use a word ”array” instead of a matrix whenever we mean a table with variables instead of constants. To encode the conditions of lemma 6 as equations, we introduce markings ${\textbf{{i}}}^{\prime}$ and ${\textbf{{f}}}^{\prime}$ (they are used to represent the intermediate markings in Lemma 6). ${\textbf{{i}}}^{\prime}$ and ${\textbf{{f}}}^{\prime}$ are arrays of variables indexed with $P\times\mathbb{Y}$. As they should be evaluated to $\mathbb{Q}^{+}$-markings we introduce inequalities ${\textbf{{i}}}^{\prime}\geq 0\text{ and }{\textbf{{f}}}^{\prime}\geq 0.$ Then it is left to encode the conditions of Lemma 6 as linear equations, which we do in two steps.

Encoding of Conditions 2, 4, 5 of lemma 6

• •

We first encode Cond. 2 of lemma 6 (the linear equation representing $\mathbb{Q}$-reachability w.r.t ${\textbf{{i}}}^{\prime},{\textbf{{f}}}^{\prime}$) as ${\textbf{{f}}}^{\prime}-{\textbf{{i}}}^{\prime}=\sum_{i=1}^{|T|}\Delta(t_{i})\cdot h_{i}\text{,}$ where $h_{i}$ are arrays of variables of dimension $\mathit{Var}\times\mathbb{Y}$ to represent histograms, since all non-zero columns appear in $\mathbb{Y}$. To guarantee that each array $h_{i}$ is encoding a histogram we add equations encoding Conditions 1 and 2 from Definition 8. We use the following notation: variable $h_{i}[r][\alpha]$ is used to indicate the entry in row $r$ and column $\alpha\in\mathbb{Y}$ of the histogram array $h_{i}$. Now, each entry is $h_{i}[r][\alpha]\geq 0$ and for every $\alpha,r,i$,

[TABLE]

• •

To encode the conditions $4,5$ of lemma 6 , we will need to allow for

implication relation between variables. Therefore, we add the constraints $\forall t_{i}\in T,\leavevmode\nobreak\ \forall p\in P,\leavevmode\nobreak\ \forall r\in\mathit{Var},\leavevmode\nobreak\ \forall\alpha\in\mathbb{Y},$

[TABLE]

This set of implications ensures that if for a $\mathbb{Q}$-run $\sigma^{\prime}$, $(p,d)\in Pre(\sigma^{\prime})$, then ${\textbf{{i}}}^{\prime}(p,d)>0$ and similarly for the post-set.

**Encoding of conditions 1 and 3 of Lemma 6:

**As these conditions are symmetric we explain in detail only the encoding of Condition 1. Knowing, $\mathit{dval}(\sigma)\subseteq\mathbb{Y}$ we may bound the number of transitions from i to ${\textbf{{i}}}^{\prime}$ by $B=|P|\cdot|\mathbb{Y}|=|P|\cdot\left(|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})|+1+\max_{t\in T}(|\mathit{vars}(t)|)\right).$ The first problem in trying to encode a run here is that, we don’t know the exact order on which transitions of $\sigma$ will be taken, the second is that we don’t know the precise instantiation of them. We handle both problems by over-approximating reachability via at most $B$ steps by a reachability via runs in following schema:

[TABLE]

where $h_{i,j}$ are histograms with columns from the set $\mathbb{Y}$ and the expression $(t_{i},h_{i,j})$ denotes any $\mathbb{Q}^{+}$-run that uses only a single transition $t_{i}$. To see that it is an over-approximation it suffices to see that any run of length at most $B$ can be performed within the schema. The mentioned over-approximation is sufficient for us due to Remark 1. The $j^{th}$ step from the run can be found in the $j^{th}$ block $\left[(t_{1},h_{1,j})\ldots(t_{|T|},h_{|T|,j})\right]$, histograms of all unnecessary transitions are instantiated to zero.

Having above we describe $\mathbb{Q}^{+}$-reachability within this schema restricted to data values from $\mathbb{Y}$. We do it by introducing sets of arrays describing configurations ${\textbf{{i}}}={\textbf{{i}}}_{0},{\textbf{{i}}}_{1},{\textbf{{i}}}_{2},\ldots,{\textbf{{i}}}_{B\cdot|T|}={\textbf{{i}}}^{\prime}$ between runs $(t_{i},h_{i,j}).$ Further, for all $0\leq i<B\cdot|T|$ we add equations ${\textbf{{i}}}_{i}+\Delta(t_{j})\cdot h_{j,k}={\textbf{{i}}}_{i+1}$ where $i=(j-1)+(k-1)\cdot|T|$ and necessary equations guaranteeing $h_{j,k}$ to be histograms (as done for $h_{i}$ above). The described system is of polynomial size and correctly captures $\mathbb{Q}$-reachability.

The last missing bit is to restrict solutions as we want to express only $\mathbb{Q}^{+}$-reachability. Of course all of ${\textbf{{i}}}_{i}$ should be non-negative so we add equations ${\textbf{{i}}}_{i}\geq 0\ \forall i\leq B\cdot|T|.$ This suffices to capture $\mathbb{Q}^{+}$-reachability. Indeed, each of $\mathbb{Q}$-runs between ${\textbf{{i}}}_{i}$ and ${\textbf{{i}}}_{i+1}$ is using a single transition, and from Lemma 7 we get that they are fireable $\mathbb{Q}^{+}$-runs.

Thus, we have correctly described $\mathbb{Q}^{+}$ reachability via the schema from i to ${\textbf{{i}}}^{\prime}$.

Finally, we obtain Theorem 3.3 as a consequence of Lemma 8 and Lemma 9.

8 Conclusion

In this paper, we provided a polynomial time algorithm for continuous reachability in UDPN, matching the complexity for Petri nets without data. This is in contrast to problems such as discrete coverability, termination, where Petri nets with and without data differ enormously in complexity, and to (discrete) reachability, whose decidability is still open for UDPN. As future work, we aim to implement the continuous reachability algorithm developed here, to build the first tool for discrete coverability in UDPN on the lines of what has been done for Petri nets without data. The main obstacle will be performance evaluation due to lack of benchmarks for UDPNs. Another interesting avenue for future work would be to tackle continuous reachability for Petri nets with ordered data, which would allow us to analyze continuous variants of Timed Petri nets and so on.

9 Appendix

9.1 Proofs from section 5

See 2

Proof

By definition of $\mathit{uniformize}$ operation, if $\alpha\not\in{\mathbb{E}}$, then

[TABLE]

The second equality is due to the definition of $\mathit{rotate}$, since data outside of ${\mathbb{E}}$ are not touched by $\mathit{rotate}$. Going further, if $\alpha\in{\mathbb{E}}$ then ${\textbf{{f}}}^{\prime}(\bullet,\alpha)-{\textbf{{i}}}^{\prime}(\bullet,\alpha)=$

[TABLE]

This completes the proof of Lemma 2. Next, we move to the important proof of Claim 1 stated in Lemma 3. We first recall the claim.

See 1

Proof (of Claim 1)

We prove this claim by induction on $j$, the number of steps fired in the run $\sigma$. Assuming $\textbf{{m}}_{j}^{\prime}$ to be as in the claim we show that $\textbf{{m}}_{j+1}^{\prime}$ satisfies the claim.

Base Case :- Initially (at marking $\textbf{{m}}_{0}={\textbf{{i}}}=\textbf{{m}}_{0}^{\prime}$). For all $\gamma\in{\mathbb{E}}\cup\{\alpha\}$ ${\textbf{{i}}}(\bullet,\gamma)=\textbf{0}$. The two first points hold trivially and for the third one we see that $\textbf{0}=\frac{1}{|{\mathbb{E}}|}\left(\sum_{\delta\in{{\mathbb{E}}}\cup\{\alpha\}}\textbf{0}\right).$ Hence, shown.

Induction step :- Let us prove the three conditions in turn.

• •

Condition 1. This is the simplest. Due to $\mathit{rot}(\alpha,{\mathbb{E}},\bullet)$ operations being a part of every step in $\rho$ we know that $\alpha$ does not participate in any step of $\rho$ so its value stays constant, and equals 0.

• •

Condition 2. Due to the definitions of $\mathit{replace},\alpha,$ and ${\mathbb{E}}$ we have that $\mathcal{R}(\alpha,{\mathbb{E}},\omega)(\bullet,\gamma)=\omega(\bullet,\gamma)$ holds for all $\gamma\in\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}}),$ where $\omega$ is any step in $\mathcal{U}({{\mathbb{E}}},\sigma_{j})$. Thus, if $\textbf{{m}}_{j}^{\prime}\xrightarrow{\mathcal{U}({{\mathbb{E}}},\sigma_{j})}_{\mathbb{Q}}\textbf{{z}}$, then we have:

[TABLE]

Now, by Lemma 2 $\forall\gamma\in\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})$ we have $\textbf{{z}}(\bullet,\gamma)-\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)=\textbf{{m}}_{j+1}(\bullet,\gamma)-\textbf{{m}}_{j}(\bullet,\gamma)$. Further, by the induction hypothesis, we have $\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)=\textbf{{m}}_{j}(\bullet,\gamma)$. Therefore $\textbf{{z}}(\bullet,\gamma)=\textbf{{m}}_{j+1}(\bullet,\gamma)$, and finally By Equation (3) above, $\textbf{{m}}_{j+1}^{\prime}(\bullet,\gamma)=\textbf{{m}}_{j+1}(\bullet,\gamma).$

• •

Condition 3. This is the most complex condition to show. Let $\beta$ be the data value which is swapped with $\alpha$ in the $\mathit{replace}$ operation, or any datum from ${\mathbb{E}}$ such that $c_{j}\Delta(t_{j})\cdot{\mathcal{P}}_{j})(\bullet,\alpha)=\textbf{0}.$ Suppose markings z and $\textbf{{z}}^{\prime}$ are such that $\textbf{{m}}_{j}^{\prime}\xrightarrow{\sigma_{j}}\textbf{{z}}\text{ and }\textbf{{m}}_{j}^{\prime}\xrightarrow{\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j})}\textbf{{z}}^{\prime}.$ Then, we observe that

$\textbf{{z}}^{\prime}(\bullet,\delta)=\textbf{{z}}(\bullet,\delta)$ for all $\delta\not\in\{\alpha,\beta\}$, 2. 2.

$\textbf{{z}}^{\prime}(\bullet,\alpha)=\textbf{0}$ indeed from the induction assumption $\textbf{{m}}_{j}^{\prime}(\bullet,\alpha)=\textbf{{m}}_{j}(\bullet,\alpha)$ $=\textbf{0}$ and according to definition $\mathit{replace}$ the step $\mathcal{R}(\alpha,{\mathbb{E}},\sigma_{j})$ does not touch tokens with data value $\alpha.$ 3. 3.

$\textbf{{z}}^{\prime}(\bullet,\beta)=\textbf{{z}}(\bullet,\beta)+(\textbf{{z}}(\bullet,\alpha)-\textbf{{m}}_{j}^{\prime}(\bullet,\alpha))=\textbf{{z}}(\bullet,\beta)+\textbf{{z}}(\bullet,\alpha),$ the first equality is due to the definition of $\mathit{replace}$ the second due to the induction assumption.

Now, combining above with Lemma 2 for all $\gamma\in{\mathbb{E}}$ we get,

[TABLE]

Using $\textbf{{m}}_{j}(\bullet,\alpha)=\textbf{0}$ ( by induction assumption) and as $\textbf{{z}}-\textbf{{m}}_{j}^{\prime}=$ $\textbf{{m}}_{j+1}-\textbf{{m}}_{j}$ we derive, $\textbf{{m}}_{j+1}^{\prime}(\bullet,\gamma)-\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)=$

[TABLE]

Moreover, for any $\gamma\in{\mathbb{E}}$ we have $\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)=\frac{1}{|{\mathbb{E}}|}\left(\sum_{\delta\in{\mathbb{E}}\cup\{\alpha\}}\textbf{{m}}_{j}(\bullet,\delta)\right)$ by the induction hypothesis. Thus, we obtain $\textbf{{m}}_{j+1}^{\prime}(\bullet,\gamma)-\textbf{{m}}_{j}^{\prime}(\bullet,\gamma)=$

[TABLE]

from which we derive $\textbf{{m}}_{j+1}^{\prime}(\bullet,\gamma)=\frac{1}{|{\mathbb{E}}|}\left(\sum_{\delta\in{\mathbb{E}}\cup\{\alpha\}}\textbf{{m}}_{j+1}(\bullet,\delta)\right)$ as required.

(end of Proof of claim1)∎

9.2 Proofs from section 6

See 4

Proof

We prove both properties separately. Let $\sum_{i=1}^{n}H_{i}=H_{0}$. We have $\mathit{row}(H_{0})=\mathit{row}(H_{i})$ (the set of row indices for all $H_{i}$ is the same) and $\mathit{col}(H_{0})=\cup_{1\leq i\leq n}\mathit{col}(H_{i})$. Thus, for each $x\in\mathit{row}(H_{0})$

[TABLE]

Hence, the first condition of Definition 8 holds in $H$.

Now we show that the second condition also holds finishing the proof. For each $\alpha\in\mathit{col}(H_{0})$,

[TABLE]

as each $H_{i}$ is a histogram. Thus the second property of the definition also holds and hence $H_{0}$ is a histogram with order $\sum_{i=1}^{n}q_{i}$.

The proof of second property is very similar to the proof of Theorem 3 in [22], the only difference is that our histograms have non-negative rational entries while there, histograms had natural entries. Here we only describe an overview of the complete argument. The proof relies on building a weighted bipartite graph from the histogram $H$ whose partite sets are row and column indices. An edge between nodes corresponding to row index $x$ and column index $\alpha$ is given a weight $H(x,\alpha)$. Now define a subset $D$ of $\mathit{col}(H)$ as $D=\{\alpha\leavevmode\nobreak\ |\leavevmode\nobreak\ \sum_{x\in\mathit{row}(H)}H(x,\alpha)=q\}$. Using Hall’s theorem one can show that there exists matchings $M_{1}$, $M_{2}$ that saturate $\mathit{row}(H)$, $D$ respectively. Using $M_{1},M_{2}$ one can obtain another matching $M$ that saturates $\mathit{row}(H)\cup D$. Now we take the minimum of edge weights in the matching, let that be $a_{1}$. Then we make two histograms from $H$ using $M$ and $a_{1}$ as follows. $M$ determines a set of row,column index pairs $E$ as follows: $(x,\alpha)\in E$ implies that the edge corresponding to the nodes representing $x$ and $\alpha$ is in $M$ and vice-verse. Construct a [$a_{1}$]-histogram $H_{1}$ having $\mathit{row}(H_{1})=\mathit{row}(H),\mathit{col}(H_{1})=\mathit{col}(H)$, and $H_{1}(x,\alpha)=a_{1}$ for $(x,\alpha)\in E$, [math] otherwise. Modify $H$ by subtracting $a_{1}$ from all entries determined by $(x,\alpha)\in E$. Now we see that $H_{1}$ is an [$a_{1}$]-histogram and $H$ is a histogram of order $q-a_{1}$. We can repeatedly apply this procedure until $H$ becomes an [$a$]-histogram itself for some $a$. This completes the description of the proof.

See 5

Proof

Due to Theorem 3.1 if there is a run then there is run that uses at most $|\mathit{dval}({\textbf{{i}}})\cup\mathit{dval}({\textbf{{f}}})|+1+\max_{t\in T}(|\mathit{vars}(t)|)$ different data values. Due to Proposition 1 there are required histograms. To prove the other direction, we just need to show that we can represent $\sum_{t\in T}\Delta(t)H_{t}$ as $\sum c_{j}\Delta(t_{j}){\mathcal{P}}_{j}$ having $c_{j}\in\mathbb{Q}^{+}$, as the latter is a sequence of $\mathbb{Q}$-steps and hence a $\mathbb{Q}$-run. To this end we just need to show that we can decompose a histogram as $H_{i}$ as $\sum_{k}c_{k}{\mathcal{P}}_{k}$ for some constants $c_{k}\in\mathbb{Q}^{+}$ and some permutation matrices ${\mathcal{P}}_{k}$. This follows from Lemma 4 as after decomposing $H_{t}$ into [$a_{j}$]-histograms we can take out $a_{j}$ and write $a_{j}\cdot{\mathcal{P}}_{j}$ where ${\mathcal{P}}_{j}$ is a permutation matrix. Thus we can decompose $H_{t}$ as $\sum_{k}c_{k}{\mathcal{P}}_{k}$. This completes our proof.

See 3.2

Proof

We use the characterization from Lemma 5. We encode the reachability problem as a system of linear inequalities.

• •

${\textbf{{f}}}-{\textbf{{i}}}=\sum_{t\in T}\Delta(t)H_{t}$.

• •

Both the conditions of definition 8 are to be satisfied for all the histograms $H_{t}$ , $t\in T$.

• •

Variables are entries of the histograms and that is why for each variable $v$, we add condition $v\in\mathbb{Q}^{+}$.

The total number of variables equals $|{\mathbb{E}}|\cdot|T|\cdot|Var|$, since $|{\mathbb{E}}|$ is polynomial (according to Lemma 5) the total number of unknowns is polynomial. Thus, the number of equations is also polynomial. Since such a system of constraints can be solved as a system of linear equations over $\mathbb{Q}^{+}$ in Ptime in the size of input[28], the $\mathbb{Q}-$reachability can be solved in Ptime as the size of input is polynomial.

9.3 Proofs from section 7.1

In this section, we prove Lemma 6. We recall the statement now.

See 6 The high level view of the proof is as follows. In the first step, we consider a special case when the $\mathbb{Q}$-reachability implies $\mathbb{Q}^{+}$-reachability between markings in Lemma 10 below. The idea for this lemma and its proof is similar to Lemma 14 from [11] (in fact it would be possible to make a reduction from our setting to the statement of the mentioned lemma but it would require restating definitions from [11]). We extend it here for UDPN. The basic idea is to fire steps in such small fractions that the number of tokens never go negative. We repeatedly fire the complete $\mathbb{Q}$-run $\sigma$ with very small fractions until we reach the required marking. The second step uses this lemma to show a weak characterization of $\mathbb{Q}^{+}$-reachability, without bounding the number of $\mathbb{Q}^{+}$-steps in Lemma 11 below. Finally, the third step is to observe that both $Pre(\sigma)$ and $Post(\sigma)$ can be bounded by $P\times\mathit{dval}(\sigma)$ we strengthen this result and obtain Lemma 6.

Lemma 10 ()

If for $\mathbb{Q}^{+}$-markings i and f, there exists a $\mathbb{Q}$-run $\sigma$ such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{Q}}{\textbf{{f}}}$ and $\forall(p,\alpha)\in Pre(\sigma),{\textbf{{i}}}(p,\alpha)>0$, $\forall(p,\alpha)\in Post(\sigma),{\textbf{{f}}}(p,\alpha)>0$, then f is $\mathbb{Q}^{+}$-reachable from i.

Proof

For the $\mathbb{Q}$-run $\sigma=\{(c_{i},t_{i},P_{i})\}_{|\sigma|}$, we define a constant $\omega$, which is the sum of all tokens consumed and produced along the path $\sigma$:

[TABLE]

Observe that for any factor $s\in\mathbb{Q}^{+}$ and any $\sigma^{\prime}$ a prefix of $\sigma$ if $\textbf{{m}}\xrightarrow{s\cdot\sigma^{\prime}}\textbf{{m}}^{\prime}$ then $\textbf{{m}}^{\prime}\geq\textbf{{m}}-s\cdot\omega;$ we use this inequality later in the proof. Let a constant $c$ be a minimal distance from the empty marking to either i or f, i.e.

[TABLE]

Let $n=\max(\lceil\frac{\omega}{c}\rceil,2).$ Finally, we define the run the $\mathbb{Q}^{+}$-run $\rho$ by firing $n-$ times the run $\frac{1}{n}{\sigma}.$ We claim that $\rho$ is the required $\mathbb{Q}^{+}$-run and is fireable at i. ${\textbf{{i}}}\xrightarrow{\rho}_{\mathbb{Q}}{\textbf{{f}}}$ trivially holds. Hence, the only question that remains is its fire-ability.

To show $\mathbb{Q}^{+}$-fireability, we consider intermediate markings:

[TABLE]

First, we observe that each $\textbf{{m}}_{i}(p,\alpha)\geq c$ for every pair $(p,\alpha)\in Pre(\sigma)\cup Post(\sigma),$ indeed $\textbf{{m}}_{i}(p,\alpha)\geq min({\textbf{{i}}}(p,\alpha),{\textbf{{f}}}(p,\alpha))\geq c$ for $(p,\alpha)\in Pre(\sigma)\cup Post(\sigma).$ So we only need to show fireability of the run $\frac{\sigma}{n}$ from $\textbf{{m}}_{i}$. But the number of tokens consumed along the run $\frac{\sigma}{n}$ is smaller than $\frac{\omega}{n}\leq\omega\cdot\frac{c}{\omega}=c$. So, the total number of consumed tokens along the run $\frac{\sigma}{n}$ is smaller than $c$ and smaller than the number of tokens in $\textbf{{m}}_{i}(p,\alpha).$ Thus $\frac{\omega}{n}$ is $\mathbb{Q}^{+}$ fireable.

Now using the above Lemma, we show a weaker characterization of $\mathbb{Q}^{+}$-reachability, without bounding the number of $\mathbb{Q}^{+}$-steps. We formalize this as:

Lemma 11

For two $\mathbb{Q}^{+}$-markings ${\textbf{{i}}},{\textbf{{f}}}$, there exists a $\mathbb{Q}^{+}$-run $\sigma$ such that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{Q}^{+}}{\textbf{{f}}}$ iff there exist markings ${\textbf{{i}}}^{\prime}$ and ${\textbf{{f}}}^{\prime}$ (possibly on a different run) such that

${\textbf{{i}}}^{\prime}$* is $\mathbb{Q}^{+}$-reachable from i* 2. 2.

There is a run $\sigma^{\prime}$ such that $\mathit{dval}(\sigma^{\prime})\subseteq\mathit{dval}(\sigma)$ and ${\textbf{{i}}}^{\prime}\xrightarrow{\sigma^{\prime}}_{\mathbb{Q}}{\textbf{{f}}}^{\prime}.$ 3. 3.

f* is $\mathbb{Q}^{+}$-reachable from ${\textbf{{f}}}^{\prime}$* 4. 4.

$\forall(p,\alpha)\in Pre(\sigma^{\prime}),{\textbf{{i}}}^{\prime}(p,\alpha)>0$** 5. 5.

$\forall(p,\alpha)\in Post(\sigma^{\prime}),{\textbf{{f}}}^{\prime}(p,\alpha)>0$**

Proof

The easy direction is that the 5 conditions imply continuous reachability. Indeed, due to Lemma 10, points $2,4,$ and $5$ imply continuous reachability from ${\textbf{{i}}}^{\prime}$ to ${\textbf{{f}}}^{\prime}$. Now, to obtain a fireable run from i to f we concatenate three runs: from i to ${\textbf{{i}}}^{\prime}$ (point 1), form ${\textbf{{i}}}^{\prime}$ to ${\textbf{{f}}}^{\prime}$, and the run from ${\textbf{{f}}}^{\prime}$ to f (point 3).

The proof in the opposite direction is more involved. Before we start it, we introduce a new operation on two sequences $\{a_{n}\},\{b_{n}\}$ where $\{a_{n}\}$ is a sequence of steps and $\{b_{n}\}$ is a sequence of real numbers, both having length $k$. We define $a_{n}\bigotimes b_{n}$ as $\{a_{1}\cdot b_{1},a_{2}\cdot b_{2},\ldots,a_{k}\cdot b_{k}\}$.

Let $\sigma=\{(c_{i},t_{i},P_{i})\}_{|\sigma|}$ where terms have their usual meanings. First, we need a small constant, namely a smallest positive number appearing in the problem definition divide by a biggest number in the problem definition

[TABLE]

In addition we define $c_{min}=\frac{1}{2}\min(1,c_{i}:\text{ where }c_{i}\text{ are coefficients in }\sigma).$

Let $\mathbb{S}_{prev}$ be a set of (place, datum) pairs which are consumed during the run but are not present in the initial configuration; similarly let $\mathbb{S}_{post}$ be a set of (place, datum) pairs which are produced during the run but do not appear in the final configuration, i.e. $\mathbb{S}_{prev}=Pre(\sigma)\setminus\{(p,\alpha):{\textbf{{i}}}(p,\alpha)>0\}$ and $\mathbb{S}_{post}=Post(\sigma)\setminus\{(p,\alpha):{\textbf{{f}}}(p,\alpha)>0\}.$ For $(p,\alpha)\in\mathbb{S}_{prev}$ the value $\textbf{{m}}(p,\alpha)$ goes from 0 to non-negative value along the run. we call the first step after which $\textbf{{m}}(p,\alpha)$ becomes positive as the marking step, and similarly un-marking steps are the steps that make $\textbf{{m}}(p,\alpha),\leavevmode\nobreak\ (p,\alpha\in\mathbb{S}_{post})$ zero for the last time. We define $\sigma_{prev}$ and $\sigma_{post}$ two subsequences of $\sigma$. $\sigma_{prev}$ is the sequence of marking steps and $\sigma_{post}$ is the sequence of un-marking steps. Finally, we define two other sequences

[TABLE]

[TABLE]

Claim 2

$\sigma_{prev}\bigotimes\omega_{prev}$* can be fired from i.*

Claim 3

m* obtained after firing $\sigma_{prev}\bigotimes\omega_{prev}$ from i is positive on all elements in $Pre(\sigma).$*

Indeed, the coefficients provided by the $\omega_{prev}$ sequence guarantee that any place that was marked during the run $\sigma_{prev}\bigotimes\omega_{prev}$ will nether get negative nor zero during the run $\sigma_{prev}$. The constant $\omega$ is used to reduce difference between the minimal amount of tokens that can be produced and the maximal amount of tokens that can be consumed in consecutive steps.

Similarly, we claim that there is $\textbf{{m}}^{\prime}$ such that $\sigma_{post}\bigotimes\omega_{post}$ can be fired firm $\textbf{{m}}^{\prime}$ and it leads to f. Indeed, it suffices to reverse direction of all transitions and look to $\sigma_{post}\bigotimes\omega_{post}$ backward.

Moreover, there is a $\mathbb{Q}$ run $\delta$ form m to $\textbf{{m}}^{\prime}$ such that $\mathit{dval}(\delta)=\mathit{dval}(\sigma)$. Indeed, $\delta$ can be obtained via removing from $\sigma$ two sequences $\sigma_{post}\bigotimes\omega_{post}$ and $\sigma_{prev}\bigotimes\omega_{prev}$. It is possible as due to constant $c_{min}$ the coefficients of any step in runs $\sigma_{post}\bigotimes\omega_{post}$ and $\sigma_{prev}\bigotimes\omega_{prev}$ are smaller than coefficients in the run $\frac{1}{2}\sigma.$ Finally, we put ${\textbf{{i}}}^{\prime}=\textbf{{m}}$, ${\textbf{{f}}}^{\prime}=\textbf{{m}}^{\prime},$ and $\sigma^{\prime}=\delta$ as $\textbf{{m}},\textbf{{m}}^{\prime}$ and $\delta$ satisfies assumptions of Lemma 10. This completes the proof of Lemma 11.

Now to obtain the proof Lemma 6 from the above Lemma, we analyze lengths of $\sigma_{prev}$ and $\sigma_{post}$ in the proof of the above Lemma. Trivially, both lengths are bounded by $|Pre(\sigma)|$ and $|Post(\sigma)|$, respectively, as each step introduces or removes a new pair $(p,\alpha)$. Further, both $|Pre(\sigma)|$ and $|Post(\sigma)|$ can be bounded by $|P\times\mathit{dval}(\sigma)|$ which is exactly what we require in the formulation of Lemma 6.

9.4 Proofs from Section 7.2

We show that every UDPN can be converted to a loop-less UDPN with the required equivalence. Transformation to a loop-less UDPN

Lemma 12 ()

For every net $N$ and two markings ${\textbf{{i}}},{\textbf{{f}}}$ in polynomial time one can construct a loop-less net $N^{\prime}$ and two markings ${\textbf{{i}}}^{\prime},\ {\textbf{{f}}}^{\prime}$ such that ${\textbf{{i}}}\xrightarrow{}_{\mathbb{Q}^{+}}{\textbf{{f}}}$ in the net $N$ iff ${\textbf{{i}}}^{\prime}\xrightarrow{}_{\mathbb{Q}^{+}}{\textbf{{f}}}^{\prime}$ in $N^{\prime}.$

Proof

We first construct the loop-less net and then show its equivalence.

Let the initial net be $N=(P,T,F,\mathit{Var})$ and markings be ${\textbf{{i}}},{\textbf{{f}}}$ and transformed net $N^{\prime}=(P_{c},T_{c},F_{c},\mathit{Var})$ and markings be ${\textbf{{i}}}^{\prime},{\textbf{{f}}}^{\prime}$. The construction is as follows.

$P_{c}=P\cup P^{\prime}$ where $|P^{\prime}|=|P|$, and for each place $p\in P$ there is a corresponding place denoted as $f(p)$, where $f$ is a relabelling operation. $P^{\prime}$ is defined as $P^{\prime}=\cup_{p\in P}f(p)$. Note that $|P_{c}|=2\cdot|P|$. 2. 2.

$T_{c}$ contains a modified transition corresponding to $T$ and an additional transition for each place. We add a transition for each place in $t$ that can remove an any data token from $f(p)$ and add it to $p$. We modify each transition $t\in T$ so that if a place $p\in PrePlace(t)\cap PostPlace(t)$ , we remove $p$ from the PostPlace and add $f(p)$ to it. This is reflected in flow relation $F_{c}$- if a place $p\in PrePlace(t)\cap PostPlace(t)$ , $F_{c}(t,f(p))=F(t,p)$ and $F_{c}(t,p)=\emptyset$. Otherwise, $F_{c}(t,p)=F(t,p)$ and $F_{c}(p,t)=F(p,t)$. Further we add $|P|$ transitions. For each $p\in P$ we define a transition as $t$ having pre-place as $f(p)$ and post-place as $p$, we add the relation $(f(p),t)\to({x}\to 1),x\in Var$ and $(t,p)\to(x\to 1)$ in $F_{c}$. This completes the construction for $T_{c},F_{c}$. Note that $|T_{c}|=|T|+|P|$. 3. 3.

We define ${\textbf{{i}}}^{\prime}$ as in i for all $p\in P\cap P_{c}$ and for the $\forall p\in P_{c}\backslash P$, we define the marking to have zero tokens for all data.i.e. $\forall p\in P,\forall d\in\mathbb{D},{\textbf{{i}}}^{\prime}(p,d)={\textbf{{i}}}(p,d)$ and $\forall p\in P_{c}\backslash P,\forall d\in\mathbb{D},{\textbf{{i}}}^{\prime}(p,d)=0$. Similarly we define ${\textbf{{f}}}^{\prime}$.

Claim 4

The $\mathbb{Q}^{+}$-reachability problem on $N$ and $N^{\prime}$ is equivalent.

Proof

Suppose that in the net $N$, f is $\mathbb{Q}^{+}$-reachable. Then we make the following modifications to the $\mathbb{Q}^{+}$-run :- We fire a transition $t$ as in the original run, after which we fire all the newly added transitions $t^{\prime}$ which are involved with only $p$ and $f(p)$) with appropriate modes so that for all $f(p)$ all the data tokens are removed from $f(p)$ and added to $p$. This is possible due to the fact that the flow relation for all such $t^{\prime}$ has only one variable in both arcs. We repeat this step for all transitions in the run. With this modification, each marking in the run has exactly the same tokens $\forall p\in P$ as in the original run after firing the transitions and [math] $\forall p\in P_{c}\backslash P$. Since $f(p)$ is not a pre-place for any transition $t$ in the original net, all transitions can be fired. By induction, we reach a ${\textbf{{f}}}^{\prime}$ having the above mentioned property corresponding to final marking f. The marking ${\textbf{{f}}}^{\prime}$ is as described by the transformation. Therefore, ${\textbf{{f}}}^{\prime}$ is $\mathbb{Q}^{+}$-reachable in $N^{\prime}$.

In the other direction, suppose it is $\mathbb{Q}^{+}$-reachable in $N^{\prime}$, then whenever a new transition $t$ is fired, a modified transition $t_{1}$ must have been fired previously. Therefore, we remove all the firings of new transitions (take a projection on $T$), and show that it remains a valid run. For a new transition to have been fired, a transition must have been fired that must have put tokens in the new place. However, in the original net, the tokens were simply added in the old place. Therefore, the transition can still be fired. Hence shown.

This completes the proof of lemma 12.

Example 3

Consider the net $N$ in Figure 2 (left). Then the net we get after the transformation is $N^{\prime}$ in Figure 2 (right).

See 7

Proof

Recall that by lemma 4, every histogram $H$ can be decomposed as $H=\sum c_{i}{\mathcal{P}}_{i}$. Therefore, applying this decomposition we get ${\textbf{{f}}}-{\textbf{{i}}}=\Delta(t)\cdot\sum c_{i}{\mathcal{P}}_{i}$. Consider a $\mathbb{Q}^{+}$-run $\sigma=\{(c_{i},t,{\mathcal{P}}_{i})\}_{|\sigma|}$ from i to f. We want to show that ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{Q}^{+}}{\textbf{{f}}}$ holds. As the net is loop-less we can split places into three kinds: places from which the run $\sigma$ consumes tokens, to which the run $\sigma$ produces, and places not touched by the run $\sigma$. For the second and third kind of places it is trivial that number of tokens with any data value is not getting negative along $\sigma.$ For the place of the first kind and for any data value observe that, along the run $\sigma$ the number of tokens in the place and with the datum can only drop. Thus, if at any moment along the run $\sigma$ it got negative then it would stay negative to the very end of $\sigma$. But in the end i.e. f it is non-negative. Thus, the number of tokens with any data value in any place along $\sigma$ stays non-negative, and ${\textbf{{i}}}\xrightarrow{\sigma}_{\mathbb{Q}^{+}}{\textbf{{f}}}$ holds.