Fundamenta Informaticae - Volume 122, issue 1-2

Authors: Kristensen, Lars Michael | Penczek, Wojciech | Petrucci, Laure

Article Type: Other

DOI: 10.3233/FI-2013-780

Citation: Fundamenta Informaticae, vol. 122, no. 1-2, pp. v-vi, 2013

Authors: Reynier, Pierre-Alain | Servais, Frédéric

Article Type: Research Article

Abstract: This paper presents the Monotone-Pruning algorithm (MP) for computing the minimal coverability set of Petri nets. The original Karp and Miller algorithm (K&M) unfolds the reachability graph of a Petri net and uses acceleration on branches to ensure termination. The MP algorithm improves the K&M algorithm by adding pruning between branches of the K&M tree. This idea was first introduced in the Minimal Coverability Tree algorithm (MCT), however it was recently shown to be incomplete. The MP algorithm can be viewed as the MCT algorithm with a slightly more aggressive pruning strategy which ensures completeness. Experimental results show that this …algorithm is a strong improvement over the K&M algorithm as it dramatically reduces the exploration tree. Show more

DOI: 10.3233/FI-2013-781

Citation: Fundamenta Informaticae, vol. 122, no. 1-2, pp. 1-30, 2013

Authors: Couvreur, Jean-Michel | Poitrenaud, Denis | Weil, Pascal

Article Type: Research Article

Abstract: We propose a new model of branching processes, suitable for describing the behavior of general Petri nets, without any finiteness or safeness assumption. In this framework, we define a new class of branching processes and unfoldings of a net N, which we call faithful. These coincide with the safe branching processes and unfoldings if N is safe, or weakly safe as in [Engelfriet 1991], but not in general. However, faithful branching processes and processes satisfy the good order-theoretic properties which make the safe processes of safe nets so useful in practice, and which are known not to hold for the …safe processes of a general net. Faithful processes represent therefore good candidates to generalize the theory of safe nets to the general case. Show more

Keywords: General Petri nets, Unfoldings, Branching processes

DOI: 10.3233/FI-2013-782

Citation: Fundamenta Informaticae, vol. 122, no. 1-2, pp. 31-58, 2013

Authors: van Hee, Kees M. | Sidorova, Natalia | van der Werf, Jan Martijn

Article Type: Research Article

Abstract: Stepwise refinement is a well-known strategy in system modeling. The refinement rules should preserve essential behavioral properties, such as deadlock freedom, boundedness and weak termination. A well-known example is the refinement rule that replaces a safe place of a Petri net with a sound workflow net. In this case a token on the refined place undergoes a procedure that is modeled in detail by the refining workflow net. We generalize this rule to component-based systems, where in the first, high-level, refinement iterations we often encounter in different components places that represent in fact the counterparts of the same procedure “simultaneously” …executed by the components. The procedure involves communication between these components. We model such a procedure as a multi-workflow net, which is actually a composition of communicating workflows. Behaviorally correct multi-workflow nets have the weak termination property. The weak termination requirement is also applied to the system being refined. We want to refine selected places in different components with a multi-workflow net in such a way that the weak termination property is preserved through refinements. We introduce the notion of synchronizable places and show that weak termination is preserved under the refinement of places with multiworks if and only if the refined places are synchronizable. We give a method to decide if a given set of places is synchronizable. Show more

DOI: 10.3233/FI-2013-783

Citation: Fundamenta Informaticae, vol. 122, no. 1-2, pp. 59-83, 2013

Authors: Peschanski, Frédéric | Klaudel, Hanna | Devillers, Raymond

Article Type: Research Article

Abstract: We present a Petri net interpretation of the pi-graphs - a graphical variant of the picalculus where recursion and replication are replaced by iteration. The concise and syntax-driven translation can be used to reason in Petri net terms about open reconfigurable systems. We demonstrate that the pi-graphs and their translated high-level Petri nets agree at the semantic level. In consequence, existing results on pi-graphs naturally extend to the translated Petri nets, most notably a guarantee of finiteness by construction.

Keywords: Reconfigurable systems, Pi-calculus, Iteration, Petri nets

DOI: 10.3233/FI-2013-784

Citation: Fundamenta Informaticae, vol. 122, no. 1-2, pp. 85-117, 2013

Authors: Kleijn, Jetty | Koutny, Maciej

Article Type: Research Article

Abstract: A concurrent history represented by a causality structure that captures the intrinsic, invariant dependencies between its actions, can be interpreted as defining a set of closely related observations (e.g., step sequences). Depending on the relationships observed in the histories of a system, the concurrency paradigm to which it adheres may be identified, with different concurrency paradigms underpinned by different kinds of causality structures. Elementary net systems with inhibitor arcs and mutex arcs (ENIM-systems) are a system model that through its process semantics and associated causality structures fits the least restrictive concurrency paradigm. One can also investigate the abstract behaviour of …an ENIM-system by grouping together step sequences in equivalence classes (generalised comtraces) using the structural relations between its transitions. The resulting concurrent histories of the ENIM-system are consistent with the generalised stratified order structures underlying its processes. The paper establishes a link between ENIM-systems and trace theory allowing one to discuss different observations of concurrent behaviour in a way that is consistent with the causality semantics defined by the operationally defined processes. Show more

Keywords: concurrency paradigm, elementary net system, inhibitor arc, mutex arc, step sequence, causality, generalised stratified order structure, process semantics, generalised comtrace

DOI: 10.3233/FI-2013-785

Citation: Fundamenta Informaticae, vol. 122, no. 1-2, pp. 119-146, 2013

Authors: Haddad, Serge | Mairesse, Jean | Nguyen, Hoang-Thach

Article Type: Research Article

Abstract: For a large Markovian model, a “product form” is an explicit description of the steady-state behaviour which is otherwise generally untractable. Being first introduced in queueing networks, it has been adapted to Markovian Petri nets. Here we address three relevant issues for product-form Petri nets which were left fully or partially open: (1) we provide a sound and complete set of rules for the synthesis; (2) we characterise the exact complexity of classical problems like reachability; (3) we introduce a new subclass for which the normalising constant (a crucial value for product-form expression) can be efficiently computed.

Keywords: Petri nets, product-form, synthesis, complexity analysis, reachability, normalising constant

DOI: 10.3233/FI-2013-786

Citation: Fundamenta Informaticae, vol. 122, no. 1-2, pp. 147-172, 2013