special issue of Petri Nets 2019
Raymond Devillers.
In order to speed up the synthesis of Petri nets from labelled transition
systems, a divide and conquer strategy consists in defining decompositions of
labelled transition systems, such that each component is synthesisable iff so
is the original system. Then corresponding Petri Net composition operators are
searched to combine the solutions of the various components
into a solution of the original system. The paper presents two such
techniques, which may be combined: products and articulations. They may also be
used to structure transition systems, and to analyse the performance of
synthesis techniques when applied to such structures.
Alain Finkel ; Serge Haddad ; Igor Khmelnitsky.
In the early two-thousands, Recursive Petri nets have been introduced in
order to model distributed planning of multi-agent systems for which counters
and recursivity were necessary. Although Recursive Petri nets strictly extend
Petri nets and context-free grammars, most of the usual problems (reachability,
coverability, finiteness, boundedness and termination) were known to be
solvable by using non-primitive recursive algorithms. For almost all other
extended Petri nets models containing a stack, the complexity of coverability
and termination are unknown or strictly larger than EXPSPACE. In contrast, we
establish here that for Recursive Petri nets, the coverability, termination,
boundedness and finiteness problems are EXPSPACE-complete as for Petri nets.
From an expressiveness point of view, we show that coverability languages of
Recursive Petri nets strictly include the union of coverability languages of
Petri nets and context-free languages. Thus we get a more powerful model than
Petri net for free.
David de Frutos Escrig ; Maciej Koutny ; Łukasz Mikulski.
In reversible computations one is interested in the development of mechanisms
allowing to undo the effects of executed actions. The past research has been
concerned mainly with reversing single actions. In this paper, we consider the
problem of reversing the effect of the execution of groups of actions (steps).
Using Petri nets as a system model, we introduce concepts related to this new
scenario, generalising notions used in the single action case. We then present
properties arising when reverse actions are allowed in place/transition nets
(pt-nets). We obtain both positive and negative results, showing that allowing
steps makes reversibility more problematic than in the interleaving/sequential
case. In particular, we demonstrate that there is a crucial difference between
reversing steps which are sets and those which are true multisets. Moreover, in
contrast to sequential semantics, splitting reverses does not lead to a general
method for reversing bounded pt-nets. We then show that a suitable solution can
be obtained by combining split reverses with weighted read arcs.
Didier Lime ; Olivier H. Roux ; Charlotte Seidner.
We investigate the problem of parameter synthesis for time Petri nets with a
cost variable that evolves both continuously with time, and discretely when
firing transitions. More precisely, parameters are rational symbolic constants
used for time constraints on the firing of transitions and we want to
synthesise all their values such that some marking is reachable, with a cost
that is either minimal or simply less than a given bound.
We first prove that the mere existence of values for the parameters such that
the latter property holds is undecidable. We nonetheless provide symbolic
semi-algorithms for the two synthesis problems and we prove them both sound and
complete when they terminate. We also show how to modify them for the case when
parameter values are integers. Finally, we prove that these modified versions
terminate if parameters are bounded. While this is to be expected since there
are now only a finite number of possible parameter values, our algorithms are
symbolic and thus avoid an explicit enumeration of all those values.
Furthermore, the results are symbolic constraints representing finite unions of
convex polyhedra that are easily amenable to further analysis through linear
programming.
We finally report on the implementation of the approach in Romeo, a software
tool for the analysis of time Petri nets.
Ronny Tredup.
For a fixed type of Petri nets $\tau$, \textsc{$\tau$-Synthesis} is the task
of finding for a given transition system $A$ a Petri net $N$ of type $\tau$
($\tau$-net, for short) whose reachability graph is isomorphic to $A$ if there
is one. The decision version of this search problem is called
\textsc{$\tau$-Solvability}. If an input $A$ allows a positive decision, then
it is called $\tau$-solvable and a sought net $N$ $\tau$-solves $A$. As a well
known fact, $A$ is $\tau$-solvable if and only if it has the so-called
$\tau$-\emph{event state separation property} ($\tau$-ESSP, for short) and the
$\tau$-\emph{state separation property} ($\tau$-SSP, for short). The question
whether $A$ has the $\tau$-ESSP or the $\tau$-SSP defines also decision
problems. In this paper, for all $b\in \mathbb{N}$, we completely characterize
the computational complexity of \textsc{$\tau$-Solvability},
\textsc{$\tau$-ESSP} and \textsc{$\tau$-SSP} for the types of pure $b$-bounded
Place/Transition-nets, the $b$-bounded Place/Transition-nets and their
corresponding $\mathbb{Z}_{b+1}$-extensions.