Fundamenta Informaticae - Volume 183, issue 1-2

Authors: Donatelli, Susanna | Haar, Stefan | Lasota, Slawomir

Article Type: Other

DOI: 10.3233/FI-2021-2079

Citation: Fundamenta Informaticae, vol. 183, no. 1-2, pp. v-vi, 2021

Authors: Devillers, Raymond

Article Type: Research Article

Abstract: 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.

Keywords: labelled transition systems, composition, decomposition, Petri net synthesis

DOI: 10.3233/FI-2021-2080

Citation: Fundamenta Informaticae, vol. 183, no. 1-2, pp. 1-31, 2021

Authors: Finkel, Alain | Haddad, Serge | Khmelnitsky, Igor

Article Type: Research Article

Abstract: 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. Show more

Keywords: Recursive Petri nets, Expressiveness, Complexity, Coverability, Termination, Finiteness

DOI: 10.3233/FI-2021-2081

Citation: Fundamenta Informaticae, vol. 183, no. 1-2, pp. 33-66, 2021

Authors: de Frutos Escrig, David | Koutny, Maciej | Mikulski, Łukasz

Article Type: Research Article

Abstract: 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. Show more

Keywords: Petri net, reversible computation, step semantics, action splitting, net synthesis, direct reversibility, mixed reversibility, weighted activator arcs

DOI: 10.3233/FI-2021-2082

Citation: Fundamenta Informaticae, vol. 183, no. 1-2, pp. 67-96, 2021

Authors: Lime, Didier | Roux, Olivier H. | Seidner, Charlotte

Article Type: Research Article

Abstract: 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. Show more

Keywords: Time Petri nets, reachability, parameters, cost, optimality

DOI: 10.3233/FI-2021-2083

Citation: Fundamenta Informaticae, vol. 183, no. 1-2, pp. 97-123, 2021

Authors: Tredup, Ronny

Article Type: Research Article

Abstract: For a fixed type of Petri nets τ , τ -SYNTHESIS is the task of finding for a given transition system A a Petri net N of type τ (τ -net, for short) whose reachability graph is isomorphic to A if there is one. The decision version of this search problem is called τ -SOLVABILITY . If an input A allows a positive decision, then it is called τ -solvable and a sought net N τ -solves A . As a well known fact, A is τ -solvable if and only if it has …the so-called τ -event state separation property (τ -ESSP, for short) and the τ -state separation property (τ -SSP, for short). The question whether A has the τ -ESSP or the τ -SSP defines also decision problems. In this paper, for all b ∈ ℕ, we completely characterize the computational complexity of τ -SOLVABILITY , τ -ESSP and τ -SSP for the types of pure b -bounded Place/Transition-nets, the b -bounded Place/Transitionnets and their corresponding ℤb +1 -extensions. Show more

Keywords: Petri nets, synthesis, b-bounded, SSP, ESSP, solvability

DOI: 10.3233/FI-2021-2084

Citation: Fundamenta Informaticae, vol. 183, no. 1-2, pp. 125-167, 2021