decisionproblem   _Input:_  _Question:_

22 2135

Synthesis with Restricted Place-environments

# Synthesis of Pure and Impure Petri nets with
Restricted Place-environments: Complexity Issues

Raymond Devillers
Département d’Informatique - Université Libre de Bruxelles
Boulevard du Triomphe  B1050 Brussels  Belgium
<EMAIL_ADDRESS>Ronny Tredup
Institut Für Informatik - Universität Rostock
Albert-Einstein-Straße 22 Address of correspondence: Institut Für Informatik -
Universität Rostock, Albert-Einstein-Straße 22, D18059 Rostock, Germany D18059
Rostock  Germany
<EMAIL_ADDRESS>
###### Abstract

Petri net synthesis consists in deciding for a given transition system $A$
whether there exists a Petri net $N$ whose reachability graph is isomorphic to
$A$. Several works examined the synthesis of Petri net subclasses that
restrict, for every place $p$ of the net, the cardinality of its preset or of
its postset or both _in advance_ by _small_ natural numbers $\varrho$ and
$\kappa$, respectively, such as for example (weighted) marked graphs,
(weighted) T-systems and choice-free nets. In this paper, we study the
synthesis aiming at Petri nets which have such restricted place environments,
from the viewpoint of classical and parameterized complexity: We first show
that, for any fixed natural numbers $\varrho$ and $\kappa$, deciding whether
for a given transition system $A$ there is a Petri net $N$ such that (1) its
reachability graph is isomorphic to $A$ and (2) for every place $p$ of $N$ the
preset of $p$ has at most $\varrho$ and the postset of $p$ has at most
$\kappa$ elements is doable in polynomial time. Secondly, we introduce a
modified version of the problem, namely Environment Restricted Synthesis (ERS,
for short), where $\varrho$ and $\kappa$ are part of the input, and show that
ERS is NP-complete, regardless whether the sought net is impure or pure. In
case of the impure nets, our methods also imply that ERS parameterized by
$\varrho+\kappa$ is $W[2]$-hard.

††volume: 187††issue: 2-4

##  1 Introduction

Petri net synthesis consists in deciding for a given transition system $A$
whether there is a Petri net $N$ such that the reachability graph of $N$ is
isomorphic to $A$. In the event of a positive decision, a possible solution
$N$ should be constructed, and in the event of a negative decision some
reason(s) should be produced if possible. Synthesis of Petri nets has
applications in various fields: For example, it is used to extract concurrency
and distributability data from sequential specifications like transition
systems or languages [1]; it is applied in the field of process discovery to
reconstruct a model from its execution traces [2] and in supervisory control
for discrete event systems [3]; and it is used for the synthesis of speed-
independent circuits [4].

The synthesis problem has been originally solved for the class of _Elementary
net systems_ [5], relying on _regions_ of transition systems, and has been
found to be NP-complete for this class in [6]. Later on, this solution was
extended to weighted P/T nets, as well as to weighted pure ones, for which,
however, the synthesis problem is solvable in polynomial time [7].

Since then, many studies have been carried out on the synthesis of
structurally restricted subclasses of Petri nets, which aim at improved (pre-)
synthesis methods with regard to the specified subclass. The most investigated
subclasses of Petri nets include those that restrict the cardinality of the
presets or the postsets of the places by _a priori_ fixed _small_ natural
numbers $\varrho$ and $\kappa$, respectively. Among them are especially the
so-called (weighted or plain) _marked graphs_ [8] (every place has exactly one
pre- and exactly one post-transition), the (weighted) _T-systems_ [9] (every
place has at most one pre- and at most one post-transition) and, as a
generalization of both, the (weighted) _choice-free_ nets [10, 11] (every
place has at most one post-transition). These restrictions are initially
motivated by the fact that, from the theoretical point of view, the resulting
net classes allow a rich and elegant theory with respect to their structure as
well as highly efficient analysis algorithms [9, 11, 12, 13, 14, 15]. From the
perspective of practical applications, they are particularly useful in, for
example, some applications like hardware design [4, 16] or as a proper model
for systems with bulk services and arrivals [11]. On the other hand, as
already mentioned, these classes have also been the subject of research aiming
at Petri net synthesis for many years [15, 17, 18, 19, 20, 21]. It turned out
that these net classes provide some very useful features like, for example,
persistency of their reachability graphs [11] that –if it comes to complexity
issues– allow improved synthesis procedures that –instead of regions– rather
rely on some basic structural properties of the input transition system. Also
the computational complexity of synthesis depending on the desired subclass
has been subject of this research: In [15], for example, it has been shown
that synthesis aiming at choice-free nets is polynomial, and in [22], for
example, it has been proved that synthesis aiming at weighted marked graphs
(or weighted $T$-systems) is polynomial when the input transition system is
circular.

In this paper, we extend the research on the computational complexity of
synthesis aiming at Petri nets with restricted place environments: We show
that, for any fixed natural numbers $\varrho$ and $\kappa$, deciding whether
for a given transition system $A$ there is a Petri net $N$ such that (1) its
reachability graph is isomorphic to $A$ and (2) for every place $p$ of $N$ the
preset of $p$ has at most $\varrho$ and the postset of $p$ has at most
$\kappa$ elements may be done in polynomial-time. In a natural way, the
question arises whether synthesis remains polynomial if the bounds $\varrho$
and $\kappa$ are not fixed in advance, but are part of the input. In this
paper, we answer this question negatively and show first for the class of
(impure) Petri nets that the corresponding decision problem (Environment
Restricted Synthesis, ERS for short) is NP-complete. We obtain this result by
methods that give also information about the parameterized complexity of ERS
parameterized by $\varrho+\kappa$ (aiming at impure nets): The proof for the
membership of ERS implies that its parameterized version belongs to the
complexity class XP. The NP-hardness of ERS results from a polynomial-time
reduction of the well-known problem Hitting Set, which is also a valid
parameterized reduction. Since Hitting Set is $W[2]$-complete, this implies
that ERS parameterized by $\varrho+\kappa$ is $W[2]$-hard. Hence,
$\varrho+\kappa$ is unsuitable for fixed parameter tractability
(FPT)-approaches as pioneered in [23, 24].

This paper is an extended version of [25]. The main new result is the proof
that ERS is NP-complete even if we restrict the addressed net class to pure
Petri nets. We obtain this result by a reduction of the problem Cubic Monotone
1 in 3 3Sat, which cannot be derived from the reduction for the impure nets.

_Further Related Work._ For net classes for which the (underlying)
unrestricted synthesis problem is already NP-complete as, for example, it is
the case for $b$-bounded Petri nets [26] or an overwhelming amount of Boolean
nets [27] the problem ERS (or its corresponding formulation) is also NP-
complete. This can easily be shown by a trivial reduction from the
unrestricted to the restricted problem. In [28], it has been shown that ERS,
formulated for $b$-bounded Petri nets, is NP-complete even if $\kappa=1$.
Moreover, in [29], it has been argued that the corresponding problem, although
being in XP, is $W[1]$-hard for these nets, when $\varrho+\kappa$ is
considered as a parameter. In [30, 31], it has been shown that the
parametrized complexity of (the Boolean formulation of) ERS is $W[1]$-hard or
$W[2]$-hard for a lot of Boolean Petri nets. However, neither of these results
imply the ones provided by the currentpaper.

This paper is organized as follows. Section 2 introduces necessary definitions
and provides some examples. After that, Section 3 provides the announced
complexity results, and Section 4 provides some results on the synthesis of
pure place-environment restricted P/T nets. Finally, Section 5 briefly closes
the paper.

##  2 Preliminaries

In this section, we introduce relevant basic notions around Petri net
synthesis and provide some examples.

######  Definition 2.1 (Transition Systems)

A (deterministic, labeled) _transition system_ (TS, for short)
$A=(S,E,\delta,\iota)$ is a directed labeled graph with the set of nodes $S$
(called _states_), the set of labels $E$ (called _events_), the partial
_transition function_ $\delta:S\times E\longrightarrow S$ and the _initial
state_ $\iota\in S$. Event $e$ _occurs_ at state $s$, denoted by
$s\leavevmode\hbox to18.33pt{\vbox
to10.26pt{\pgfpicture\makeatletter\hbox{\hskip 1.10999pt\lower-1.47998pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{ }{}{{
{\pgfsys@beginscope\pgfsys@setlinewidth{0.24pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{}
{}{}{} {}{}{}
\pgfsys@moveto{-1.10999pt}{1.47998pt}\pgfsys@curveto{-1.01749pt}{0.92499pt}{0.0pt}{0.0925pt}{0.2775pt}{0.0pt}\pgfsys@curveto{0.0pt}{-0.0925pt}{-1.01749pt}{-0.92499pt}{-1.10999pt}{-1.47998pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}$, if $\delta(s,e)$ is
defined. By $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{3.34007pt}{2.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{{$\scalebox{0.8}{$\neg
e$}$}} }}\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}}$, we denote that $e$
does not occur at $s$. We abridge $\delta(s,e)=s^{\prime}$ by
$s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}$ and call
the latter an _edge_. By $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}\in A$, we
denote that the edge $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}$ is present
in $A$. We say $A$ is _loop-free_ if $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}\in A$
implies $s\not=s^{\prime}$. A sequence $s_{0}\leavevmode\hbox to17.37pt{\vbox
to11.55pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.77655pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.5534pt}{2.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{{$\scalebox{0.8}{$e_{1}$}$}} }}\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}}s_{1},s_{1}\leavevmode\hbox
to17.37pt{\vbox to11.55pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.77655pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.5534pt}{2.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{{$\scalebox{0.8}{$e_{2}$}$}} }}\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}}s_{2},\dots,s_{n-1}\leavevmode\hbox
to17.37pt{\vbox to11.07pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.29742pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.32887pt}{2.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{{$\scalebox{0.8}{$e_{n}$}$}} }}\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}}s_{n}$ of edges is
called a (directed labeled) _path_ (from $s_{0}$ to $s_{n}$ in $A$). $A$ is
called _initialized_ if, for every state $s\in S$, we have $s=\iota$ or there
is a path from $\iota$ to $s$.

If a TS $A$ is not explicitly defined, then we refer to its components by
$S(A)$ (states), $E(A)$ (events), $\delta_{A}$ (function), $\iota_{A}$
(initial state). In this paper, we investigate whether a TS corresponds to the
reachability graph of a Petri net. Since the latter are always initialized, we
assume that all TS are initialized without explicitly mentioning this each
time. We shall only consider finite TS, i.e., that $S$ and $E$ (hence also
$\delta$) are finite. Moreover, we consider TS $A$ and $B$ to be essentially
the same when isomorphic:

######  Definition 2.2 (Isomorphic TS)

Two TS $A=(S,E,\delta,\iota)$ and
$B=(S^{\prime},E,\delta^{\prime},\iota^{\prime})$ with the same set of events
are _isomorphic_ , denoted by $A\cong B$, if there is a bijection
$\varphi:S\rightarrow S^{\prime}$ such that $\varphi(\iota)=\iota^{\prime}$
and $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}\in A$ if
and only if $\varphi(s)\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}\varphi(s^{\prime})\in
B$.

Starting from a certain behavior that is defined by a transition system, we
look for a machine that implements this behavior, namely a Petri net (more
exactly a weighted P/T net):

######  Definition 2.3 (Petri Nets)

A _Petri net_ $N=(P,T,f,M_{0})$ consists of finite and disjoint sets of
_places_ $P$ and _transitions_ $T$, a (total) _flow_ $f:((P\times
T)\cup(T\times P))\rightarrow\mathbb{N}$ (interpreted as denoting the number
of _tokens_ absorbed and produced by $t$ on $p$) and an _initial marking_
$M_{0}:P\rightarrow\mathbb{N}$ (more generally, a marking is any function
$M:P\rightarrow\mathbb{N}$).
The _preset_ of a place $p$ is defined by $\,{}^{\\!\bullet}p=\\{t\in T\mid
f(t,p)>0\\}$, thus comprising all the transitions that produce tokens on $p$,
while the _postset_ of $p$ is defined by $p^{\bullet}=\\{t\in T\mid
f(p,t)>0\\}$, thus comprising all the transitions that consume tokens from
$p$. Notice that $\,{}^{\\!\bullet}p\cap p^{\bullet}$ is not necessarily
empty, but if this is true for each place $p\in P$ the net is said _pure_. For
$\varrho,\kappa\in\mathbb{N}$, we say $p$ is _$(\varrho,\kappa)$ -restricted_
if $|\,^{\\!\bullet}p|\leq\varrho$ and $|p^{\bullet}|\leq\kappa$; note that it
is also possible to only constrain the size of $\,{}^{\\!\bullet}p$ or
$p^{\bullet}$, by considering $(\varrho,|T|)$-restricted and
$(|T|,\kappa)$-restricted nets.
A transition $t\in T$ can _fire_ or _occur_ in a marking
$M:P\rightarrow\mathbb{N}$, denoted by $M\leavevmode\hbox to17.37pt{\vbox
to11.59pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{7.09146pt}{2.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{{$\scalebox{0.8}{$t$}$}} }}\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}}$, if $M(p)\geq
f(p,t)$ for all places $p\in P$. The firing of $t$ in marking $M$ leads to the
marking $M^{\prime}(p)=M(p)-f(p,t)+f(t,p)$ for all $p\in P$, denoted by
$M\leavevmode\hbox to17.37pt{\vbox
to11.59pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{7.09146pt}{2.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{{$\scalebox{0.8}{$t$}$}} }}\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^{\prime}$. This
notation extends to sequences $w\in T^{*}$ and the _reachability set_
$RS(N)=\\{M\mid\exists w\in T^{*}:M_{0}\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.5646pt}{2.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{{$\scalebox{0.8}{$w$}$}} }}\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\\}$ contains all
reachable markings of $N$. The _reachability graph_ of $N$ is the TS
$A_{N}=(RS(N),T,\delta,M_{0})$, where for every reachable marking $M$ of $N$
and transition $t\in T$ with $M\leavevmode\hbox to17.37pt{\vbox
to11.59pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{7.09146pt}{2.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{{$\scalebox{0.8}{$t$}$}} }}\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^{\prime}$ the
transition function $\delta$ of $A_{N}$ is defined by $\delta(M,t)=M^{\prime}$
($\delta(M,t)$ being undefined if $t$ may not fire in $M$).

According to Definition 2.3, for every Petri net, there is a TS, that reflects
the global behavior of the net, namely its reachability graph. However, not
every TS is the behavior of a Petri net and thus the following decision
problem arises:

If Synthesis allows a positive decision, then we want to construct $N$ purely
from $A$: $N$ is then called a _solution_ of $A$. When there is a solution,
there are infinitely many of them, sometimes with very different structure,
and it may be interesting to restrict the target class of a synthesis problem,
like the $(\rho,\kappa)$-restricted class for instance. Note that, since we
only consider a finite TS $A$, its solutions are always bounded, meaning that,
for some integer $k$, we have $M(p)\leq k$ for each place $p$ and reachable
marking $M$. Since $A$ and $A_{N}$ should be isomorphic, the events $E$ of $A$
become the transitions of $N$. Note however that $A$ does not allow to answer
all questions about its solutions: since we work up to isomorphism it is not
possible to state if some marking is reachable or dominated, but since $A$ is
finite it will be easy to answer such questions when $N$ will be chosen.

The places, the flow and the initial marking of $N$, hence the solutions of
$A$, originate from so-called _regions_ of the TS $A$.

######  Definition 2.4 (Region)

A _region_ $R=(sup,con,pro)$ of a TS $A=(S,E,\delta,\iota)$ consists of three
mappings _sup port_ $sup:S\rightarrow\mathbb{N}$, _con sume_
$con:E\rightarrow\mathbb{N}$ and _pro duce_ $pro:E\rightarrow\mathbb{N}$, such
that if $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}$ is an edge
of $A$, then $con(e)\leq sup(s)$ and $sup(s^{\prime})=sup(s)-con(e)+pro(e)$.
The _preset_ of $R$ is defined by $\,{}^{\\!\bullet}R=\\{e\in E\mid
pro(e)>0\\}$ and its _postset_ by $R^{\bullet}=\\{e\in E\mid con(e)>0\\}$. A
region is _pure_ if $\,{}^{\\!\bullet}R\cap R^{\bullet}=\emptyset$. For
$\varrho,\kappa\in\mathbb{N}$, we shall say that $R$ is _$(\varrho,\kappa)$
-restricted_ if $|\,^{\\!\bullet}R|\leq\varrho$ and $|R^{\bullet}|\leq\kappa$.

###### Remark 2.5

Notice that _if_ $R=(sup,con,pro)$ _is_ a region of a TS
$A=(S,E,\delta,\iota)$, _then_ $R$ can be obtained from $sup(\iota)$, $con$,
and $pro$: Since $A$ is initialized, for every state $s\in S$, there is a path
$\iota\leavevmode\hbox to17.37pt{\vbox
to11.55pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.77655pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.5534pt}{2.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{{$\scalebox{0.8}{$e_{1}$}$}} }}\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}}\dots\leavevmode\hbox
to17.37pt{\vbox to11.07pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.29742pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.32887pt}{2.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{{$\scalebox{0.8}{$e_{n}$}$}} }}\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}}s_{n}$ such that
$s=s_{n}$. Hence, we inductively obtain $sup(s_{i+1})$ by
$sup(s_{i+1})=sup(s_{i})-con(e_{i+1})+pro(e_{i+1})$ for all
$i\in\\{0,\dots,n-1\\}$ and $s_{0}=\iota$. For brevity, we shall often use
this observation and present regions only _implicitly_ by $sup(\iota)$, $con$
and $pro$. When a region will be defined that way, it will be necessary to
check that such a definition is coherent, i.e., each computed support is non-
negative and if two edges lead to the same state this also leads to the same
support; such checks will however be usually easy. For an even more compact
presentation, for $c,p\in\mathbb{N}$, we shall group events with the same
“behavior” together by $\mathcal{T}_{c,p}^{R}=\\{e\in E\mid con(e)=c\text{ and
}pro(e)=p\\}$.

Regions of the TS become places in a sought net if it exists: for a place
$R=(sup,con,pro)$ of such a net, $con(e)$ defines $f(R,e)$, the number of
tokens that $e$ consumes from $R$, and $pro(e)$ defines $f(e,R)$, the number
of tokens that $e$ produces on $R$, and $sup(s)$ models (the number of tokens)
$M(R)$ (that are on $R$) in the marking $\varphi(s)=M$ of $N$ that corresponds
to state $s$ of $A$ via the isomorphism $\varphi$ between $A$ and $A_{N}$.

######  Definition 2.6 (Synthesized Net)

Every set $\mathcal{R}$ of regions of a TS $A$ defines the _synthesized net_
$N^{\mathcal{R}}_{A}=(\mathcal{R},E,f,M_{0})$ with $f(R,e)=con(e)$,
$f(e,R)=pro(e)$ and $M_{0}(R)=sup(\iota)$ for all
$R=(sup,con,pro)\in\mathcal{R}$ and all $e\in E$.

In order to ensure that the input behavior $A$ is correctly captured by a
synthesized net $N$, meaning that $A$ and $A_{N}$ are identified by an
isomorphism $\varphi$, we have to ensure that distinct states
$s\not=s^{\prime}$ of $A$ correspond to distinct markings
$\varphi(s)\not=\varphi(s^{\prime})$ of $N$. In particular, we need $A$ to
have the _state separation property_ , which means that its _state separation
atoms_ are solvable:

######  Definition 2.7 (State Separation)

A pair $(s,s^{\prime})$ (unordered) of distinct states of $A$ defines a _state
separation atom_ (SSA). There are thus $|S|\cdot(|S|-1)/2$ such SSA’s. A
region $R=(sup,con,pro)$ _solves_ $(s,s^{\prime})$ if
$sup(s)\not=sup(s^{\prime})$. We say a state $s$ is _solvable_ if, for every
$s^{\prime}\in S\setminus\\{s\\}$, there is a region that solves the SSA
$(s,s^{\prime})$. If every SSA or, equivalently, every state of $A$ is
solvable then $A$ has the _state separation property_ (SSP).

Furthermore, we have to prevent the firing of a transition in a marking $M$,
if its corresponding event does not occur at the state $s$ of $A$ that
corresponds to $M$ via the isomorphism $\varphi$, that is, if
$s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{3.34007pt}{2.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{{$\scalebox{0.8}{$\neg
e$}$}} }}\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}}$, then
$\varphi(s)\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{3.34007pt}{2.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{{$\scalebox{0.8}{$\neg
e$}$}} }}\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}}$, where
$\varphi(s)=M$. In particular, $A$ must have the _event/state separation
property_ , meaning that all _event/state separation atoms_ of $A$ are
solvable:

######  Definition 2.8 (Event/State Separation)

A pair $(e,s)$ of event $e\in E$ and state $s\in S$ such that
$s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{3.34007pt}{2.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{{$\scalebox{0.8}{$\neg
e$}$}} }}\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}}$ defines an
_event/state separation atom_ (ESSA). There are thus $|S|\cdot|E|-|\delta|$
such ESSA’s (where $|\delta|$ is the number of pairs $(s,e)$ such that
$\delta(s,e)$ is defined). A region $R=(sup,con,pro)$ _solves_ $(e,s)$ if
$sup(s)<con(e)$. We say an event $e$ is _solvable_ if, for all $s\in S$ such
that $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{3.34007pt}{2.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{{$\scalebox{0.8}{$\neg
e$}$}} }}\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}}$, there is a region
that solves the ESSA $(e,s)$. If every ESSA or, equivalently, every event of
$A$ is solvable then $A$ has the _event state separation property_ (ESSP).

######  Definition 2.9 (Admissible set)

A set $\mathcal{R}$ of regions of $A$ is called _admissible_ if it witnesses
the SSP and the ESSP of $A$, that is, every SSA and ESSA of $A$ is solvable by
a region $R$ of $\mathcal{R}$.

The next lemma, borrowed from [32, p. 162] but also present in [33],
establishes the connection between the existence of an admissible set
$\mathcal{R}$ of $A$ and the existence of a Petri net $N$ whose rechability
graph is isomorphic to $A$. Notice that Petri nets correspond to the type of
nets $\tau_{PT}$ in [32, p. 130].

######  Lemma 2.10 ([32])

If $A$ is a TS and $N$ a Petri net, then $A\cong A_{N}$ if and only if there
is an admissible set $\mathcal{R}$ of $A$ and $N=N^{\mathcal{R}}_{A}$.

By Lemma 2.10, deciding the existence of a sought net $N$ for $A$ is
equivalent to deciding the existence of an admissible set $\mathcal{R}$ of
$A$. Moreover, since the regions $R=(sup,con,pro)$ of $\mathcal{R}$ yield the
places in $N=N_{A}^{\mathcal{R}}$ and the corresponding flow is defined by
$con$ and $pro$, the places of $N$ are $(\varrho,\kappa)$-restricted if and
only if every region $R\in\mathcal{R}$ is $(\varrho,\kappa)$-restricted.
Eventually, this leads us to the following decision problem, which is the main
subject of this paper:

$A_{1}:$

$\boldsymbol{s_{0}}$

$s_{1}$

$s_{2}$

$a$

$b$

$a$

$A_{2}:$

$\boldsymbol{s_{0}}$

$s_{1}$

$a$

$a$

$A_{3}:$

$\boldsymbol{s_{0}}$

$s_{1}$

$s_{2}$

$s_{3}$

$a$

$b$

$b$

$a$

Figure 1: The TS $A_{1}$ (Example 2.11), $A_{2}$ (Example 2.12) and $A_{3}$
(Example 2.13) (initial states are indicated in bold).

$N_{1}:$$R_{1}$$a$

1

$R_{3}$

1

1

$R_{2}$$b$

1

$A_{N_{1}}:$$\boldsymbol{111}$$011$$101$$001$

$a$

$b$

$b$

$a$

Figure 2: Left: The Petri Net $N_{1}$ with initial marking
$M_{0}(R_{1})M_{0}(R_{2})M_{0}(R_{3})=111$ and $(1,1)$-restricted places.
Right: The reachability graph $A_{N_{1}}$.

$N_{2}:$$R_{1}$$a$

1

$R_{2}$$b$

1

$A_{N_{2}}:$$\boldsymbol{11}$$01$$10$$00$

$a$

$b$

$b$

$a$

Figure 3: Left: The Petri Net $N_{2}$ with initial marking
$M_{0}(R_{1})M_{0}(R_{2})=11$ and $(0,1)$-restricted places. Right: The
reachability graph $A_{N_{2}}$.

###### Example 2.11

The TS $A_{1}$ of Figure 3 has neither the SSP nor the ESSP: If
$R=(sup,con,pro)$ is a region of $A_{1}$, then the edge $s_{0}\leavevmode\hbox
to17.37pt{\vbox to10.11pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.42155pt}{2.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{{$\scalebox{0.8}{$a$}$}} }}\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}}s_{0}$ requires
$sup(s_{0})=sup(s_{0})-con(a)+pro(a)$, implying $con(a)=pro(a)$. The latter
implies $sup(s_{1})=sup(s_{2})$ by $sup(s_{2})=sup(s_{1})-con(a)+pro(a)$.
Moreover, by $s_{1}\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.42155pt}{2.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{{$\scalebox{0.8}{$a$}$}} }}\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}}$, we have
$sup(s_{1})\geq con(a)$ and thus $sup(s_{2})\geq con(a)$. Consequently, since
$R$ was arbitrary, the SSA $(s_{1},s_{2})$ and the ESSA $(a,s_{2})$ are not
solvable.

###### Example 2.12

The TS $A_{2}$ of Figure 3 has the ESSP by triviality, since the only event
$a$ occurs at all states of $A_{2}$, but not the SSP: The SSA $(s_{0},s_{1})$
is not solvable, since any region $R=(sup,con,pro)$ of $A_{2}$ satisfies
$sup(s_{0})=sup(s_{1})-con(a)+pro(a)$ and
$sup(s_{1})=sup(s_{0})-con(a)+pro(a)$, which implies $sup(s_{0})=sup(s_{1})$.

###### Example 2.13

The TS $A_{3}$ of Figure 3 has the ESSP and the SSP: The region
$R_{1}=(sup_{1},con_{1},pro_{1})$, which, according to Remark 2.5, is
implicitly given by $sup_{1}(s_{0})=1$ and $\mathcal{T}_{1,0}^{R_{1}}=\\{a\\}$
and $\mathcal{T}_{0,0}^{R_{1}}=\\{b\\}$, solves $(a,s_{1})$, $(a,s_{3})$,
$(s_{0},s_{1})$, $(s_{0},s_{3})$, $(s_{2},s_{1})$ and $(s_{2},s_{3})$. We
obtain $R_{1}$ explicitly by
$sup_{1}(s_{1})=sup_{1}(s_{0})-con_{1}(a)+pro_{1}(a)=0$ and
$sup_{1}(s_{2})=sup(s_{0})-con_{1}(b)+pro_{1}(b)=1$ and
$sup_{1}(s_{3})=sup_{1}(s_{2})-con_{1}(a)+pro_{1}(a)=0$.

Moreover, the region $R_{2}=(sup_{2},con_{2},pro_{2})$, which is defined by
$sup_{2}(s_{0})=sup_{2}(s_{1})=1$, $sup_{2}(s_{2})=sup_{2}(s_{3})=0$ and
$\mathcal{T}_{1,0}^{R_{2}}=\\{b\\}$ and $\mathcal{T}_{0,0}^{R_{2}}=\\{a\\}$,
solves the remaining SSA $(s_{0},s_{2})$ and $(s_{1},s_{3})$ and ESSA
$(b,s_{2})$ and $(b,s_{3})$ of $A$.

The TS $A_{3}$ has also the region $R_{3}=(sup_{3},con_{3},pro_{3})$ defined
by $sup_{3}(s_{i})=1$ for all $i\in\\{0,1,2,3\\}$ and
$\mathcal{T}_{1,1}^{R_{3}}=\\{a\\}$ and $\mathcal{T}_{0,0}^{R_{3}}=\\{b\\}$.

Since $R_{1}$ and $R_{2}$ solve all SSA and ESSA both of
$\mathcal{R}_{1}=\\{R_{1},R_{2},R_{3}\\}$ and
$\mathcal{R}_{2}=\\{R_{1},R_{2}\\}$ are admissible sets of $A_{3}$. Figure 3
shows the synthesized net $N_{1}=N^{\mathcal{R}_{1}}_{A_{3}}$ whose places are
$(1,1)$-restricted, but not $(0,1)$-restricted, since
$|\,^{\\!\bullet}R_{3}|=|\\{a\\}|=1$. The reachability graph $A_{N_{1}}$ is
sketched on the right hand side of Figure 3 and it is isomorphic to $A_{3}$.
The isomorphism $\varphi$ is given by $\varphi(s_{0})=111$,
$\varphi(s_{1})=011$, $\varphi(s_{2})=101$ and $\varphi(s_{3})=001$. However,
the input $(A_{3},0,1)$ for Environment Restricted Synthesis allows a positive
decision, because the admissible set $\mathcal{R}_{2}$ satisfies
$|\,^{\\!\bullet}R|=0$ and $|R^{\bullet}|=1$ for all $R\in\mathcal{R}_{2}$.
Figure 3 shows the synthesized net $N_{2}=N^{\mathcal{R}_{2}}_{A_{3}}$ (left)
and its reachability graph $A_{N_{2}}$ (right).

##  3 The computational complexity of Environment Restricted
Synthesis

The following theorem provides the main contribution of this section:

###### Theorem 3.1

Environment Restricted Synthesis is NP-complete.

In order to prove Theorem 3.1, we have to show that ERS is in NP and that it
is NP-hard. The following Section 3.1 is dedicated to the membership in NP.
The corresponding proof basically extends the deterministic polynomial-time
algorithm for the (unrestricted) Synthesis to a non-deterministic algorithm
for ERS. The applied methods also show that, for any fixed $\varrho$ and
$\kappa$, environment restricted synthesis can be done in polynomial-time.
After that, Section 3.2 deals with the hardness part and provides a polynomial
reduction of the Hitting Set problem.

###  3.1 Environment Restricted Synthesis is in NP

In this section, we show that ERS belongs to the complexity class NP. In order
to obtain a fitting non-deterministic algorithm for ERS, we extend the
deterministic approach for the (unrestricted) Synthesis, which, for example,
has been presented in [32]. The tractability of Synthesis is based on the fact
that the solvability of a single (state or event/state) separation atom
$\alpha$ of a given TS $A=(S,E,\delta,\iota)$ is polynomial-time reducible to
a system $L_{\alpha}$ composed of a polynomial number of linear equations and
inequalities on rational variables. Such a system can be solved or decided
unsolvable in polynomial-time by Khachiyan’s method and theorem [34, pp.
168-170]. Since $A$ has at most $|E|\cdot|S|+|S|^{2}$ separation atoms, it
follows that deciding the solvability of $A$ by deciding the solvability of
every atom via the solvability of its corresponding systems $L_{\alpha}$,
yields a deterministic polynomial-time algorithm for Synthesis (as well as a
method to produce a solution when the decision is positive). For a separation
atom $\alpha$, our approach extends the aforementioned system $L_{\alpha}$
non-deterministically to a system $L_{\alpha}^{\prime}$. The additional linear
inequalities encode the restriction requirements: $L_{\alpha}^{\prime}$ is
solvable if and only if there is a properly restricted region that solves
$\alpha$. The size of $L_{\alpha}^{\prime}$ is still polynomially bounded by
the size of $A$ and can again be solved with Khachiyan’s method. Hence, the
membership of ERS in NP follows.

In the following, unless explicitly stated otherwise, let $(A,\varrho,\kappa)$
be an arbitrary but fixed input of ERS with TS
$A=(S,\\{e_{1},\dots,e_{n}\\},\delta,\iota)$, and let $\alpha$ be an arbitrary
but fixed separation atom of $A$. In order to develop the announced approach,
we first briefly recapitulate the deterministic approach to

solve $\alpha$ by a region, which is not necessarily restricted. While we are
only informally providing the intended functionality of all equations and
inequalities presented, the formal proofs for the corresponding statements can
be found in [32]. After that, we introduce the announced extension of this
approach.

First, by Remark 2.5, a region $R=(sup,con,pro)$ is completely defined by
$sup(\iota)$, $con$ and $pro$, i.e., by $2\cdot n+1$ variables. Hence, $R$ can
be identified with a vector

$\textbf{x}=(sup(\iota),con(e_{1}),\dots,con(e_{n}),pro(e_{1}),\dots,pro(e_{n}))\in\mathbb{N}^{2n+1}$

The aforementioned system $L_{\alpha}$ essentially consists of two parts: The
first part consists of equations and inequalities that ensure that a solution
can be interpreted as a region at all. Among others, this part encompasses
equations that result from _fundamental cycles_ , which are defined by
_chords_ of a _spanning tree_ of $A$. The second part consists of an
inequality that ensures that such a region actually solves $\alpha$.

A spanning tree of a TS is a sub-TS whose underlying undirected and unlabeled
graph is a tree in the common graph-theoretical sense that is rooted at
$\iota$:

######  Definition 3.2 (Spanning tree, chord)

A _spanning tree_ $A^{\prime}=(S,E^{\prime},\delta^{\prime},\iota)$ of the TS
$A$ is a loop-free TS such that, for all $s,s^{\prime}\in S$ and all $e\in
E^{\prime}$ the following is satisfied: (1) if $s\leavevmode\hbox
to17.37pt{\vbox to10.11pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}\in
A^{\prime}$, then $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}\in A$; (2)
either $s=\iota$ or there is exactly one directed labeled path $P_{s}$ from
$\iota$ to $s$ in $A^{\prime}$. An edge $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}$ that is
present in $A$ but not in $A^{\prime}$ is called a _chord_ (for $A^{\prime}$).

In the following, let $A^{\prime}$ be an arbitrary but fixed spanning tree of
$A$. By Definition 3.2, $A^{\prime}$ contains $|\delta^{\prime}|=(|S|-1)$
edges, and $(|\delta|-|S|+1)$ chords. Moreover, for every state $s\in
S\setminus\\{\iota\\}$, there is exactly one path $P_{s}$ from $\iota$ to $s$
in $A^{\prime}$. In order to count, for every event $e\in E$, the number of
its occurrences along $P_{s}$, we use a _Parikh-vector_ :

######  Definition 3.3 (Parikh-vector)

Let $s\in S$, and let $P_{s}=\iota\leavevmode\hbox to17.37pt{\vbox
to12.41pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-3.63522pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.2617pt}{2.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{{$\scalebox{0.8}{$e_{i_{1}}$}$}} }}\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}}\dots\leavevmode\hbox
to17.37pt{\vbox to12.14pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-3.36145pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{4.77783pt}{2.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{{$\scalebox{0.8}{$e_{i_{m}}$}$}} }}\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}}s$ be the unique path
from $\iota$ to $s$ in $A^{\prime}$ if $s\not=\iota$. The _Parikh-vector_
$\psi_{s}$ (of $s$ in $A^{\prime}$) is the mapping
$\psi_{s}:\\{e_{1},\dots,e_{n}\\}\rightarrow\mathbb{N}$ defined, for every
$e\in\\{e_{1},\dots,e_{n}\\}$, by

$\psi_{s}(e)=\begin{cases}|\\{\ell\mid e_{i_{\ell}}=e\text{ and
}\ell\in\\{1,\dots,m\\}\\}|,&\text{if }s\not=\iota\\\ 0,&\text{
otherwise}\end{cases}$

For convenience we denote $\psi_{s}=(\psi_{s}(e_{1}),\dots,\psi_{s}(e_{n}))$.

The chords for $A^{\prime}$ define so-called _fundamental cycles_ :

###### Definition 3.4

Let $t=s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}$ be a chord
for $A^{\prime}$. The _fundamental cycle_ $\psi_{t}$ (of $t$) is the mapping
$\psi_{t}:\\{e_{1},\dots,e_{n}\\}\rightarrow\mathbb{Z}$ defined, for all
$i\in\\{1,\dots,n\\}$, by

$\psi_{t}(e_{i})=\begin{cases}\psi_{s}(e_{i})-\psi_{s^{\prime}}(e_{i}),&\text{if
}e_{i}\not=e\\\
\psi_{s}(e)+1-\psi_{s^{\prime}}(e),&\text{otherwise}\end{cases}$

For convenience, we denote $\psi_{t}=(\psi_{t}(e_{1}),\dots,\psi_{t}(e_{n}))$.

A region $R=(sup,con,pro)$ of $A$ is completely defined from $sup(\iota)$ and
$con,pro$ as follows:
If $\iota\leavevmode\hbox to17.37pt{\vbox
to11.55pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.77655pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.30156pt}{2.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{{$\scalebox{0.8}{$a_{1}$}$}} }}\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}}s_{1}\leavevmode\hbox
to17.37pt{\vbox to11.55pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.77655pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.30156pt}{2.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{{$\scalebox{0.8}{$a_{2}$}$}} }}\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}}\dots\leavevmode\hbox
to17.37pt{\vbox to11.07pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.29742pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{4.4548pt}{2.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{{$\scalebox{0.8}{$a_{m}$}$}} }}\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}}s$ is the unique path
$P_{s}$ from $\iota$ to $s$ in $A^{\prime}$, then

$sup(s)=sup(\iota)-con(a_{1})+pro(a_{1})\dots-con(a_{m})+pro(a_{m})$ (1)

If we define
$\textbf{z}=(pro(e_{1})-con(e_{1}),\dots,pro(e_{n})-con(e_{n}))(\in\mathbb{Z}^{n})$,
then Equation 1 reduces to

$sup(s)=sup(\iota)+\psi_{s}\cdot\textbf{z}$ (2)

with the classical scalar product of two vectors in $\mathbb{Z}^{n}$:
$(x_{1},\dots,x_{n})\cdot(y_{1},\dots,y_{n})=x_{1}\cdot y_{1}+\dots+x_{n}\cdot
y_{n}$.

Armed with these notions, we are now able to introduce $L_{\alpha}$. For the
sake of simplicity, we first restrict ourselves to the case that $\alpha$
equals an (arbitrary but fixed) ESSA $(e_{j},q)$ of $A$, where
$j\in\\{1,\dots,n\\}$. We will see later that the following arguments also
apply to SSA.

For every fundamental cycle $\psi_{t}$ of $A^{\prime}$, $L_{\alpha}$ has the
following equation:

$\psi_{t}\cdot(x_{n+1}-x_{1},\dots,x_{2n}-x_{n})=0$ (3)

Each variable must be nonnegative, hence

$\displaystyle 0\leq\,\underbrace{x_{0}}_{sup(\iota)}\land\,\,\forall
i\in\\{1,\dots,n\\}:\,0\leq$
$\displaystyle\,\underbrace{x_{i}}_{con(e_{i})}\land\,0\leq\,\underbrace{x_{n+i}}_{pro(e_{i})}$
(4)

Moreover, for all $s\in S$ and $i\in\\{1,\dots,n\\}$ with $s\leavevmode\hbox
to17.37pt{\vbox to11.59pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.81033pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.90169pt}{2.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{{$\scalebox{0.8}{$e_{i}$}$}} }}\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}}$ in $A$ (where
$e_{i}$ is not necessarily defined at $s$ in $A^{\prime}$), $L_{\alpha}$ has
the following inequalities:

$\displaystyle 0\leq$
$\displaystyle\,\underbrace{x_{0}+\psi_{s}\cdot(x_{n+1}-x_{1},\dots,x_{2n}-x_{n})}_{sup(s)}-\underbrace{x_{i}}_{con(e_{i})}$
(5)

Finally, for the ESSA $\alpha$, $L_{\alpha}$ has following inequality:

$\displaystyle\underbrace{x_{0}+\psi_{q}\cdot(x_{n+1}-x_{1},\dots,x_{2n}-x_{n})}_{sup(q)}-\underbrace{x_{j}}_{con(e_{j})}<0$
(6)

If $R$ solves $\alpha$, then
$\textbf{y}=(sup(\iota),con(e_{1}),\dots,con(e_{n}),pro(e_{1}),\dots,pro(e_{n}))$
solves $L_{\alpha}$: Equation 3 follows by Proposition 6.16 of [32]; Equation
4, Equation 5 and Equation 6 follow from Equation 2, the definition of
regions, implying $sup(\iota)\geq 0$ and $con(e_{i})\leq sup(s)$ for every
state $s$ of $A$ at which $e_{i}$ occurs, and the fact that $R$ solves
$\alpha$, implying $sup(q)<con(e_{j})$ and thus $sup(q)-con(e_{j})<0$.

Furthermore, if $\textbf{x}=(x_{0},x_{1},\dots,x_{n},x_{n+1},\dots,x_{2n})$ is
an integer solution of the system $L_{\alpha}$, then
$(sup(\iota),con(e_{1}),\dots,con(e_{n}),pro(e_{1}),\dots,pro(e_{n}))=\textbf{x}$
(implicitly) defines a region of $A$ that solves $\alpha$ [32]: Equation 3,
ensures that defining $sup(s)$ for all $s\in S$ according to Equation 2 yields
a support $sup$ that satisfies $sup(s^{\prime})=sup(s)-con(e)+pro(e)$ for
every edge $s\leavevmode\hbox to17.37pt{\vbox
to10.11pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.6734pt}{2.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{{$\scalebox{0.8}{$e$}$}} }}\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}}s^{\prime}$ of $A$ (no
incoherence may occur from different paths to the same state). Equation 4
ensures a valid support value for $\iota$. Equations 5 ensures $sup(s)\geq
con(e_{i})$ if the event $e_{i}$ occurs at $s$ in $A$ and, by $sup(\iota)\geq
0$, the equations also ensure $sup(s)\geq 0$ for all $s\in S$. Hence, the
result $R=(sup,con,pro)$ is a well-defined region of $A$. Moreover, Equation 6
implies that $R$ solves $\alpha$.

Consequently, an integer vector x solves the system built by the Equations 1-6
if and only if
$\textbf{x}=(sup(\iota),con(e_{1}),\dots,con(e_{n}),pro(e_{1}),\dots,pro(e_{n}))$
for some region $R=(sup,con,pro)$ of $A$ that solves $\alpha$.

For an SSP $\alpha=(s,s^{\prime})$, we simply have to replace constraint (6)
by the following, which expresses that the corresponding supports are
different

$\displaystyle(\psi_{s}-\psi_{s^{\prime}})\cdot(x_{n+1}-x_{1},\dots,x_{2n}-x_{n})\neq
0$ (7)

The solution of each separation problem (decision and construction if
positive) thus always amounts to solving an integer linear programming (ILP
for short) problem [35], of a size linear in the size of $A$ (without an
economic function to optimize, but we may always add a null function for
that). It may also be considered as an instance of a satisfiability modulo
theory (SMT for short) [36]. There are many ILP- or SMT-solvers111If a solver
does not allow strict comparators, it is always possible to replace “$<0$” by
“$\leq-1$”, and “$\neq 0$” by two systems, one with “$\leq-1$” and one with
“$\geq 1$” that may be used to solve such systems. Note that, in practice, it
is not necessary to handle each separation problem from scratch: it is a good
idea to first check if one of the regions found previously does not also solve
the separation atom at hand. It is also possible to handle the various
separation problems in parallel, and if $A$ presents some symmetries it is
often possible to use them to simplify the searches.

Those problems are generally NP-complete, hence they are always in NP, but
some subclasses may be polynomial and this is the case in our context. Indeed,
it may be observed that our systems are homogeneous (no constant arises, but
$0$). Hence, if we have a solution, we shall get another one by multiplying
the first one by a strictly positive scalar. That means that, instead of
searching a solution in the integer domain, we may always search one in the
rational domain, and afterwards multiply it by an adequate factor to get an
integer solution. Moreover, since there is a single strict constraint (the one
corresponding to the separation property under consideration), we may always
replace the constraint $expr<0$ by $expr\leq-1$ and replace each SSA system by
two systems with $expr\leq-1$ and $expr\geq 1$. The reason for the replacement
is that in the rational domain, there are polynomial algorithms to solve such
systems of linear constraint, like Khachiyan’s method [34, pp. 168-170].

Now let’s deduce the announced non-deterministic polynomial-time algorithm
that decides whether $\alpha$ is solvable by a $(\varrho,\kappa)$-restricted
region. If $R$ is such a region, that is, $|\,^{\\!\bullet}R|\leq\varrho$ and
$|R^{\bullet}|\leq\kappa$, then there are at most $\varrho$ indices
$i_{1},\dots,i_{\varrho}\in\\{1,\dots,n\\}$ and at most $\kappa$ indices
$j_{1},\dots,j_{\kappa}\in\\{1,\dots,n\\}$, such that $pro(e_{i_{\ell}})>0$
for all $\ell\in\\{1,\dots,\varrho\\}$ and $con(e_{j_{k}})>0$ for all
$k\in\\{1,\dots,\kappa\\}$, respectively. In particular, for all
$i\in\\{1,\dots,n\\}\setminus\\{i_{1},\dots,i_{\varrho}\\}$ and all
$j\in\\{1,\dots,n\\}\setminus\\{j_{1},\dots,j_{\kappa}\\}$, the searched
vector x solves the following equations, in addition to (3) - (6 or 7):

$\displaystyle x_{j}$ $\displaystyle=0$ (8) $\displaystyle x_{i+n}$
$\displaystyle=0$ (9)

The corresponding system $L^{\prime}_{\alpha}$ is still homogeneous, and again
it has an integer solution if and only if it has a rational solution which may
be decided and constructed in polynomial time in term of the size of $A$. The
corresponding region $R$ will then be a $(\varrho,\kappa)$-restricted region
of $A$ solving the separation problem $\alpha$, detected and built
polynomially.

Obviously, if $R$ exists, then a Turing machine $T$ can guess the indices
$i_{1},\dots,i_{\varrho}$ and $j_{1},\dots,j_{\kappa}$ in a non-deterministic
computation. After that, $T$ can deterministically construct
$L^{\prime}_{\alpha}$ and compute an integer solution x, if it exists. The
construction of $L^{\prime}_{\alpha}$ (after the aforementioned indices are
guessed) and the computation of a solution x of $L_{\alpha}^{\prime}$ as well
as the verification that x actually defines a sought region are doable in
polynomial-time. Altogether, we have argued, that the solvability of a
separation property of $A$ by a $(\varrho,\kappa)$-restricted region can be
decided by a non-deterministic Turing-machine in polynomial-time.

Let $m=|A|$ denote the size of the input TS $A=(S,E,\delta,\iota)$, implying
$|E|=n\leq m$. If $\varrho$ and $\kappa$ are fixed in advance, then there are
$\binom{n}{\varrho}$ and $\binom{n}{\kappa}$ possibilities to choose
$\\{e_{i_{1}},\dots,e_{i_{\varrho}}\\}$ and
$\\{e_{j_{1}},\dots,e_{j_{\kappa}}\\}$, respectively. Hence, in order to
decide whether $\alpha$ is solvable by a properly restricted region, we have
to check the solvability of at most $\mathcal{O}(m^{\varrho+\kappa})$ systems
of equations and inequalities like the ones discussed above. For every system,
its construction and the test of its solvability can be done deterministically
in time polynomial in $m$. Moreover, every solution of a system implies a
solving region and there are at most $|S|\cdot|E|+|S|^{2}$ separation atoms
(and this number obviously depends polynomially on $m$). Finally, by Lemma
2.10, any admissible set $\mathcal{R}$ implies already a sought net
$N=N_{A}^{\mathcal{R}}$. Therefore, this implies that there is a constant $c$
and an algorithm that (deterministically) solves ERS in time
$\mathcal{O}(m^{\varrho+\kappa+c})$ and we have the following corollary:

###### Corollary 3.5

For any fixed natural numbers $\varrho$ and $\kappa$, there is a constant $c$
and an algorithm that runs in time $\mathcal{O}(m^{c})$ and decides whether
for a given transition system $A$ there is a Petri net $N$ such that (1) the
reachability graph of $N$ is isomorphic to $A$ and (2) every place $p$ of $N$
satisfies $|\,^{\\!\bullet}p|\leq\varrho$ and $|p^{\bullet}|\leq\kappa$ and,
in the event of a positive decision, constructs a sought net $N$.

From the well-known symmetry property $\binom{n}{k}=\binom{n}{n-k}$, we deduce
more generally that

###### Corollary 3.6

For any fixed natural numbers $\varrho$ and $\kappa$, there is a polynomial
algorithm that decides whether for a given transition system $A$ there is a
Petri net $N$ such that (1) the reachability graph of $N$ is isomorphic to $A$
and (2) every place $p$ of $N$ satisfies $|\,^{\\!\bullet}p|\leq n_{1}$ and
$|p^{\bullet}|\leq n_{2}$ and, in the event of a positive decision, constructs
a sought net $N$, for the pairs $(n_{1},n_{2})=(\varrho,\kappa)$ or
$(|E|-\varrho,\kappa)$ or $(\varrho,|E|-\kappa)$ or $(|E|-\varrho,|E|-\kappa)$
or $(|E|,\kappa)$ or $(\varrho,|E|)$ or $(|E|,|E|-\kappa)$ or
$(|E|-\varrho,|E|)$.

This argument is valid if $\varrho$ and $\kappa$ are fixed in advance, but
might fail in some cases where $\varrho$ and $\kappa$ rely on the size of the
TS $A$ to be solved. For instance, if $\varrho=|E|/2$, there are
$\binom{|E|}{|E|/2}$ ways to choose $\\{e_{i_{1}},\dots,e_{i_{|E|/2}}\\}$, and
$\binom{|E|}{|E|/2}$ grows like $(4^{|E|})/\sqrt{\pi\cdot|E|/2}$, hence
exponentially (it is close to the Catalan number $C_{|E|/2}$). This is not a
proof that the problem is exponential and not polynomial, since there could be
another way to tackle the problem, but should make us suspicious. And we shall
show in the next subsection that the problem is indeed NP-complete when
$\varrho$ and $\kappa$ are given together with $A$.

###  3.2 Environment Restricted Synthesis is NP-hard

In order to complete the proof of Theorem 3.1, it remains to show that ERS is
NP-hard. Our proof of the NP-hardness will be based on a polynomial-time
reduction of the hitting set problem, which is known to be NP-complete (see
[37]):

###### Example 3.7

The instance $(\mathfrak{U},M,3)$ such that
$\mathfrak{U}=\\{X_{0},X_{1},X_{2},X_{3}\\}$ and $M=\\{M_{0},\dots,M_{5}\\}$,
where $M_{0}=\\{X_{0},X_{1}\\}$, $M_{1}=\\{X_{0},X_{2}\\}$,
$M_{2}=\\{X_{0},X_{3}\\}$, $M_{3}=\\{X_{1},X_{2}\\}$,
$M_{4}=\\{X_{1},X_{3}\\}$ and $M_{5}=\\{X_{2},X_{3}\\}$, allows a positive
decision: $\mathfrak{S}=\\{X_{0},X_{1},X_{2}\\}$ is a suitable hitting set.

In the remainder of this section, until stated explicitly otherwise, let
$(\mathfrak{U},M,\lambda)$ be an arbitrary but fixed input of HS such that
$\mathfrak{U}=\\{X_{0},\dots,X_{n-1}\\}$ and $M=\\{M_{0},\dots,M_{m-1}\\}$,
where $M_{i}=\\{X_{i_{0}},\dots,X_{i_{m_{i}-1}}\\}$ (and thus $|M_{i}|=m_{i}$)
for all $i\in\\{0,\dots,m-1\\}$. For technical reasons, we assume without loss
of generality that $i_{0}<\dots<i_{m_{i}-1}$ for the elements
$X_{i_{0}},\dots,X_{i_{m_{i}-1}}$ of the set $M_{i}$ for all
$i\in\\{0,\dots,m-1\\}$. Moreover, still for technical reasons, we assume that
$\lambda\geq 5$. Notice that this is not a restriction of the generality,
since the hitting set problem is polynomial for every fixed $\lambda$ [38].

###### Remark 3.8

Obviously, the input of Example 3.7 does not satisfy $\lambda\geq 5$. However,
in order to be able to provide a complete example of the reduction despite the
space restrictions, this input is deliberately chosen to be small.

The Reduction. In order to prove the hardness part of Theorem 3.1, we start
from input $(\mathfrak{U},M,\lambda)$ and construct an input
$(A,\varrho,\kappa)$ such that the elements of $\mathfrak{U}$ (plus some
others) occur as events in the TS $A$. Moreover, by construction, the TS $A$
has an ESSA $\alpha$ such that the following implication is true: If
$R=(sup,con,pro)$ is a region such that $|\,^{\\!\bullet}R|\leq\varrho$ and
$|R^{\bullet}|\leq\kappa$ that solves $\alpha$, then the set
$\mathfrak{S}=\\{X\in\mathfrak{U}\mid pro(X)>0\\}$ is a sought HS with at most
$\lambda$ elements for $(\mathfrak{U},M)$. Consequently, if
$(A,\varrho,\kappa)$ allows a positive decision, then there is an admissible
set of regions $\mathcal{R}$ whose pre- and postsets are accordingly
restricted. In particular, there is a region $R\in\mathcal{R}$ that solves
$\alpha$ and thus proves that $(\mathfrak{U},M,\lambda)$ also allows a
positive decision. Conversely, we argue that if $(\mathfrak{U},M,\lambda)$ has
a fitting hitting set, then there is an admissible set $\mathcal{R}$ of $A$
such that $|\,^{\\!\bullet}R|\leq\varrho$ and $|R^{\bullet}|\leq\kappa$ for
all $R\in\mathcal{R}$. Altogether, this approach proves that
$(\mathfrak{U},M,\lambda)$ is a yes-instance if and only if
$(A,\varrho,\kappa)$ is a yes-instance. Hence, if we were to have a polynomial
algorithm to decide ERS, we would also have one for HS, which is impossible.

$f_{0,0}$

$f_{0,1}$

$k$

$k_{0}$

$z_{0}$

$f_{1,0}$

$f_{1,1}$

$k$

$k_{1}$

$z_{1}$

$f_{2,0}$

$f_{2,1}$

$k$

$k_{2}$

$z_{2}$

$\top_{0}$

$\top_{1}$

$\top_{2}$

$b_{0}$

$b_{1}$

$b_{2}$

$\bot_{0}$

$\bot_{1}$

$\bot_{2}$

$\bot_{3}$

$\bot_{4}$

$\bot_{5}$

$t_{0,0}$

$t_{0,1}$

$t_{0,2}$

$t_{0,3}$

$t_{0,4}$

$t_{1,0}$

$t_{1,1}$

$t_{1,2}$

$t_{1,3}$

$t_{1,4}$

$t_{2,0}$

$t_{2,1}$

$t_{2,2}$

$t_{2,3}$

$t_{2,4}$

$t_{3,0}$

$t_{3,1}$

$t_{3,2}$

$t_{3,3}$

$t_{3,4}$

$t_{4,0}$

$t_{4,1}$

$t_{4,2}$

$t_{4,3}$

$t_{4,4}$

$t_{5,0}$

$t_{5,1}$

$t_{5,2}$

$t_{5,3}$

$t_{5,4}$

$y_{0}$

$k$

$X_{0}$

$X_{1}$

$k$

$y_{1}$

$k$

$X_{0}$

$X_{2}$

$k$

$y_{2}$

$k$

$X_{0}$

$X_{3}$

$k$

$y_{3}$

$k$

$X_{1}$

$X_{2}$

$k$

$y_{4}$

$k$

$X_{1}$

$X_{3}$

$k$

$y_{5}$

$k$

$X_{2}$

$X_{3}$

$k$

$a_{0}$

$a_{1}$

$a_{2}$

$w_{1}$

$w_{2}$

$w_{3}$

$w_{4}$

$w_{5}$

$u_{1}$

$u_{2}$

$u_{3}$

$u_{4}$

$u_{5}$

$g_{1,0}$

$g_{1,1}$

$u_{1}$

$v_{1}$

$g_{2,0}$

$g_{2,1}$

$u_{2}$

$v_{2}$

$g_{3,0}$

$g_{3,1}$

$u_{3}$

$v_{3}$

$g_{4,0}$

$g_{4,1}$

$u_{4}$

$v_{4}$

$g_{5,0}$

$g_{5,1}$

$u_{5}$

$v_{5}$

$\triangle_{1}$

$\triangle_{2}$

$\triangle_{3}$

$\triangle_{4}$

$\triangle_{5}$

$d_{1}$

$d_{2}$

$d_{3}$

$d_{4}$

$d_{5}$

$c_{1}$

$c_{2}$

$c_{3}$

$c_{4}$

$c_{5}$

Figure 4: The TS $A$ with initial state $\bot_{0}$ that results from Example
3.7. Based on the $3$-HS $\\{X_{0},X_{1},X_{2}\\}$ for $(\mathfrak{U},M)$, the
colored area sketches the region $R_{1}$ of Fact 1 that solves $(k,t_{0,1})$:
the support of the states in the green colored area equals $1$, states in the
blue colored area have support $2$, and the other ones have support $0$.

First of all, we define $\varrho=2\cdot\lambda$ and $\kappa=\lambda+1$. Notice
that this implies $\varrho\geq 10$ and $\kappa\geq 6$, since we assume
$\lambda\geq 5$. However, that does not restrict the generality, since ERS is
polynomial for any fixed integers. Figure 4 provides a complete example for
the following construction, which is based on the input of Example 3.7. The TS
$A$ has, for every $i\in\\{0,\dots,m-1\\}$, the following gadget $T_{i}$ that
represents the set $M_{i}=\\{X_{i_{0}},\dots,X_{i_{m_{i}-1}}\\}$ by using its
elements as events (between two occurrences of the event $k$):

$T_{i}=$

$t_{i,0}$

$t_{i,1}$

$\dots$$t_{i,m_{i}+1}$$t_{i,m_{i}+2}$

$k$

$X_{i_{0}}$

$X_{i_{m_{i}-1}}$

$k$

In particular, $T_{0}$ provides the ESSA $\alpha=(k,t_{0,1})$. Additionally,
the states $t_{i,1}$ and $t_{i+1,1}$ are connected by an $u_{i+1}$-labeled
edge $t_{i,1}\leavevmode\hbox to18.51pt{\vbox
to11.96pt{\pgfpicture\makeatletter\hbox{\hskip 0.72087pt\lower-3.18365pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{2.61214pt}{2.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{{$\scalebox{0.8}{$u_{i+1}$}$}} }}\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}}t_{i+1,1}$ for all
$i\in\\{0,\dots,m-2\\}$. Moreover, for every $i\in\\{0,\dots,\lambda-1\\}$,
the TS $A$ has the gadget $F_{i}$ and, for every $j\in\\{1,\dots,m-1\\}$, it
has the gadget $G_{j}$ that uses the event $u_{j}$ again:

$F_{i}=$

$f_{i,0}$

$f_{i,1}$

$k$

$k_{i}$

$z_{i}$

$G_{j}=$

$g_{j,0}$

$g_{j,1}$

$u_{j}$

$v_{j}$

The functional part of $A$ is given by the introduced gadgets. The initial
state of $A$ is $\bot_{0}$. In order to connect the gadgets, we use the
following edges that introduce fresh events and states: For every
$i\in\\{0,\dots,m-1\\}$, the TS $A$ has the edges $\bot_{i}\leavevmode\hbox
to17.37pt{\vbox to11.67pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.88855pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.65956pt}{2.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{{$\scalebox{0.8}{$y_{i}$}$}} }}\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}}t_{i,0}$ and, if
$i<m-1$, the edge $\bot_{i}\leavevmode\hbox to19.88pt{\vbox
to11.96pt{\pgfpicture\makeatletter\hbox{\hskip 1.40233pt\lower-3.18365pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{1.93068pt}{2.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{{$\scalebox{0.8}{$w_{i+1}$}$}} }}\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}}\bot_{i+1}$; the TS
$A$ has the edge $\bot_{0}\leavevmode\hbox to17.37pt{\vbox
to11.55pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.77655pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.30156pt}{2.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{{$\scalebox{0.8}{$a_{0}$}$}} }}\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}}\top_{0}$ and, for
every $i\in\\{0,\dots,\lambda-1\\}$, it has the edge $\top_{i}\leavevmode\hbox
to17.37pt{\vbox to13.7pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-2.81033pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.04753pt}{2.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{{$\scalebox{0.8}{$b_{i}$}$}} }}\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}}f_{i,0}$ and, if
$i<\lambda-1$, it has the edge $\top_{i}\leavevmode\hbox to18.16pt{\vbox
to11.96pt{\pgfpicture\makeatletter\hbox{\hskip 0.5454pt\lower-3.18365pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{2.78761pt}{2.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{{$\scalebox{0.8}{$a_{i+1}$}$}} }}\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}}\top_{i+1}$; the TS
$A$ has the edge $\bot_{0}\leavevmode\hbox to17.37pt{\vbox
to11.55pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.77655pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.68489pt}{2.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{{$\scalebox{0.8}{$c_{1}$}$}} }}\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}}\triangle_{1}$ and,
for every $i\in\\{1,\dots,m-1\\}$, it has the edge
$\triangle_{i}\leavevmode\hbox to17.37pt{\vbox
to13.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.81033pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.68225pt}{2.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{{$\scalebox{0.8}{$d_{i}$}$}} }}\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}}g_{i,0}$ and if
$i<m-1$, then it has the edge $\triangle_{i}\leavevmode\hbox to17.4pt{\vbox
to11.96pt{\pgfpicture\makeatletter\hbox{\hskip 0.16206pt\lower-3.18365pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{3.17094pt}{2.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{{$\scalebox{0.8}{$c_{i+1}$}$}} }}\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}}\triangle_{i+1}$. By
$S$ and $E$ we refer to the (set of) states and (set of) events of $A$,
respectively.

###### Lemma 3.9

If there is an admissible set of $(\varrho,\kappa)$-restricted regions for
$A$, then there is a hitting set with at most $\lambda$ elements for
$(\mathfrak{U},M)$.

###### Proof 3.10

Let $\mathcal{R}$ be an admissible set of $A$ that satisfies
$|\,^{\\!\bullet}R|\leq\varrho$ and $|R^{\bullet}|\leq\kappa$ for all
$R\in\mathcal{R}$. Since $\mathcal{R}$ is admissible, there is an accordingly
restricted region that solves the atom $\alpha=(k,t_{0,1})$. Let
$R=(sup,con,pro)$ be such a region, that is $con(k)>sup(t_{0,1})$,
$|\,^{\\!\bullet}R|\leq 2\cdot\lambda$ and $|R^{\bullet}|\leq\lambda+1$. In
the following, we argue that $\mathfrak{S}=\\{X\in\mathfrak{U}\mid
pro(X)>0\\}$ defines a sought hitting set for $(\mathfrak{U},M)$.

Since $k$ occurs at $t_{0,0}$ and $R$ solves $\alpha$, the following is true:
(1) $con(k)\leq sup(t_{0,0})$
(2) $sup(t_{0,1})=sup(t_{0,0})-con(k)+pro(k)$
(3) $con(k)>sup(t_{0,1})$.
By combining (1) and (2), we obtain $sup(t_{0,1})\geq pro(k)$. If we combine
the latter with (3), then we get $con(k)>pro(k)$. For all
$i\in\\{0,\dots,\lambda-1\\}$, by $con(k)>pro(k)$ and $f_{i,0}\leavevmode\hbox
to17.37pt{\vbox to12.22pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.32758pt}{2.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{{$\scalebox{0.8}{$k$}$}} }}\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}}f_{i,1}$, we conclude
$sup(f_{i,0})>sup(f_{i,1})$, since $sup(f_{i,1})=sup(f_{i,0})-con(k)+pro(k)$.
This implies $con(k_{i})>pro(k_{i})$ as well as $con(z_{i})<pro(z_{i})$; thus
$k_{i}\in R^{\bullet}$ and $z_{i}\in\,^{\\!\bullet}R$ for all
$i\in\\{0,\dots,\lambda-1\\}$. Since $k\in R^{\bullet}$, this implies already
$|R^{\bullet}|=\lambda+1$. In particular, no further event can be a member of
$R^{\bullet}$. Let $i\in\\{1,\dots,m-1\\}$ be arbitrary but fixed. If
$pro(u_{i})>con(u_{i})$, then we obtain $sup(g_{i,0})>sup(g_{i,1})$ and thus
$con(v_{i})>pro(v_{i})$ by $g_{i,1}\leavevmode\hbox to17.37pt{\vbox
to11.59pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.81033pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.47437pt}{2.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{{$\scalebox{0.8}{$u_{i}$}$}} }}\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}}g_{i,0}$ and
$g_{i,0}\leavevmode\hbox to17.37pt{\vbox
to11.59pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.81033pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.6818pt}{2.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{{$\scalebox{0.8}{$v_{i}$}$}} }}\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}}g_{i,1}$. This would
imply $v_{i}\in R^{\bullet}$ and $|R^{\bullet}|\geq\lambda+2$, a
contradiction. Hence, we have $pro(u_{i})\leq con(u_{i})$. By
$t_{i-1,1}\leavevmode\hbox to17.37pt{\vbox
to11.59pt{\pgfpicture\makeatletter\hbox{\hskip 0.15pt\lower-2.81033pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{5.47437pt}{2.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{{$\scalebox{0.8}{$u_{i}$}$}} }}\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}}t_{i,1}$, this implies
$sup(t_{i-1,1})\geq sup(t_{i,1})$. Since $i$ was arbitrary, we get
$sup(t_{0,1})\geq sup(t_{1,1})\geq\dots\geq sup(t_{m-1,1})$. By
$con(k)>sup(t_{0,1})$, this implies $con(k)>sup(t_{i,1})$ for all
$i\in\\{0,\dots,m-1\\}$. Furthermore, since $t_{i,m_{i}+1}\leavevmode\hbox
to17.37pt{\vbox to12.22pt{\pgfpicture\makeatletter\hbox{\hskip
0.15pt\lower-1.33301pt\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\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{}
{{}{}}{}{}{}{{{}{}}}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.3pt}\pgfsys@invoke{
}{}{}{}{}{{}}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{16.67432pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.67432pt}{0.0pt}\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}{6.32758pt}{2.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{{$\scalebox{0.8}{$k$}$}} }}\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}}$, we have $con(k)\leq
sup(t_{i,m_{i}+1})$ for all $i\in\\{0,\dots,m-1\\}$. Consequently, there has
to be at least one event $X\in\\{X_{i_{0}},\dots,X_{i_{m_{i}-1}}\\}$ such that
$pro(X)>0$. This implies $\mathfrak{S}\cap M_{i}\not=\emptyset$ for all
$i\in\\{0,\dots,m-1\\}$, where $\mathfrak{S}=\\{X\in\mathfrak{U}\mid
pro(X)>0\\}$. Moreover, since $z_{i}\in\,^{\\!\bullet}R$ for all
$i\in\\{0,\dots,\lambda-1\\}$ and $\mathfrak{S}\subseteq\,^{\\!\bullet}R$ and
$|\,^{\\!\bullet}R|\leq 2\cdot\lambda$, we have that
$|\mathfrak{S}|\leq\lambda$. This proves the claim and thus the lemma.

In order to show that all ESSA are solvable by $(\varrho,\kappa)$-restricted
regions, provided there is a fitting hitting set for $(\mathfrak{U},M)$, we
treat the events of $A$ individually. Recall that an event is solvable if all
its corresponding ESSA are solvable (Definition 2.8). Moreover, for a region
$R=(sup,con,pro)$ of $A$, the set $\mathcal{T}_{c,p}^{R}$ contains the events
$e\in E$ such that $(con(e),pro(e))=(c,p)$ (Remark 2.5).

###### Fact 1

If there is a hitting set with at most $\lambda$ elements for
$(\mathfrak{U},M)$, then the event $k$ is solvable by
$(\varrho,\kappa)$-restricted regions.

###### Proof 3.11

Let $\mathfrak{S}$ be a hitting set with at most $\lambda$ elements for
$(\mathfrak{U},M)$.

The following region $R_{0}=(sup_{0},con_{0},pro_{0})$ solves $(k,s)$ for all
$s\in\bigcup_{i=1}^{m-1}S(G_{i})$ and all
$s\in\\{\top_{0},\dots,\top_{\lambda-1}\\}$ and all
$s\in\\{\triangle_{1},\dots,\triangle_{m-1}\\}$: $sup_{0}(\bot_{0})=1$ and
$\mathcal{T}_{1,1}^{R_{0}}=\\{k\\}$ and
$\mathcal{T}_{0,1}^{R_{0}}=\\{b_{0},\dots,b_{\lambda-1}\\}$ and
$\mathcal{T}_{1,0}^{R_{0}}=\\{a_{0},c_{1}\\}$ and
$\mathcal{T}_{0,0}^{R_{0}}=E\setminus(\mathcal{T}_{1,1}^{R_{1}}\cup\mathcal{T}_{0,1}^{R_{1}}\cup\mathcal{T}_{1,0}^{R_{1}})$.
This region satisfies $|\,^{\\!\bullet}R_{0}|=\lambda+1\leq 2\cdot\lambda$ and
$|R_{0}^{\bullet}|=3$.