special issue of Petri Nets 2019

In order to speed up the synthesis of Petri nets from labelled transitionsystems, a divide and conquer strategy consists in defining decompositions oflabelled transition systems, such that each component is synthesisable iff sois the original system. Then corresponding Petri Net composition operators aresearched to combine the solutions of the various components into a solution of the original system. The paper presents two suchtechniques, which may be combined: products and articulations. They may also beused to structure transition systems, and to analyse the performance ofsynthesis techniques when applied to such structures.

In the early two-thousands, Recursive Petri nets have been introduced inorder to model distributed planning of multi-agent systems for which countersand recursivity were necessary. Although Recursive Petri nets strictly extendPetri nets and context-free grammars, most of the usual problems (reachability,coverability, finiteness, boundedness and termination) were known to besolvable by using non-primitive recursive algorithms. For almost all otherextended Petri nets models containing a stack, the complexity of coverabilityand termination are unknown or strictly larger than EXPSPACE. In contrast, weestablish 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 ofRecursive Petri nets strictly include the union of coverability languages ofPetri nets and context-free languages. Thus we get a more powerful model thanPetri net for free.

In reversible computations one is interested in the development of mechanismsallowing to undo the effects of executed actions. The past research has beenconcerned mainly with reversing single actions. In this paper, we consider theproblem 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 newscenario, generalising notions used in the single action case. We then presentproperties arising when reverse actions are allowed in place/transition nets(pt-nets). We obtain both positive and negative results, showing that allowingsteps makes reversibility more problematic than in the interleaving/sequentialcase. In particular, we demonstrate that there is a crucial difference betweenreversing steps which are sets and those which are true multisets. Moreover, incontrast to sequential semantics, splitting reverses does not lead to a generalmethod for reversing bounded pt-nets. We then show that a suitable solution canbe obtained by combining split reverses with weighted read arcs.

We investigate the problem of parameter synthesis for time Petri nets with acost variable that evolves both continuously with time, and discretely whenfiring transitions. More precisely, parameters are rational symbolic constantsused for time constraints on the firing of transitions and we want tosynthesise all their values such that some marking is reachable, with a costthat is either minimal or simply less than a given bound. We first prove that the mere existence of values for the parameters such thatthe latter property holds is undecidable. We nonetheless provide symbolicsemi-algorithms for the two synthesis problems and we prove them both sound andcomplete when they terminate. We also show how to modify them for the case whenparameter values are integers. Finally, we prove that these modified versionsterminate if parameters are bounded. While this is to be expected since thereare now only a finite number of possible parameter values, our algorithms aresymbolic and thus avoid an explicit enumeration of all those values.Furthermore, the results are symbolic constraints representing finite unions ofconvex polyhedra that are easily amenable to further analysis through linearprogramming. We finally report on the implementation of the approach in Romeo, a softwaretool for the analysis of time Petri nets.

For a fixed type of Petri nets $\tau$, \textsc{$\tau$-Synthesis} is the taskof 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 thereis one. The decision version of this search problem is called\textsc{$\tau$-Solvability}. If an input $A$ allows a positive decision, thenit is called $\tau$-solvable and a sought net $N$ $\tau$-solves $A$. As a wellknown 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 questionwhether $A$ has the $\tau$-ESSP or the $\tau$-SSP defines also decisionproblems. In this paper, for all $b\in \mathbb{N}$, we completely characterizethe computational complexity of \textsc{$\tau$-Solvability},\textsc{$\tau$-ESSP} and \textsc{$\tau$-SSP} for the types of pure $b$-boundedPlace/Transition-nets, the $b$-bounded Place/Transition-nets and theircorresponding $\mathbb{Z}_{b+1}$-extensions.