Abstract:
Model checking is an important aim of the theoretical computer science. It enables the verification of a model with a set of properties such as liveness, deadlock or safety. One of the typical modelling techniques are Petri nets they are well understood and can be used for a model checking. Reconfigurable Petri nets are based on a Petri nets with a set of rules. These rules can be used dynamically to change the net. Missing is the possibility to verify a reconfigurable net and properties such as deadlocks or liveness. This paper introduces a conversion from reconfigurable Petri net to Maude, that allows us to fill the gap. It presents a net transformation approach which is based on Maude's equation- and rewrite logic as well as the LTLR model checker.

Abstract:
In this paper the correspondence between safe Petri nets and event structures, due to Nielsen, Plotkin and Winskel, is extended to arbitrary nets without self-loops, under the collective token interpretation. To this end we propose a more general form of event structure, matching the expressive power of such nets. These new event structures and nets are connected by relating both notions with configuration structures, which can be regarded as representations of either event structures or nets that capture their behaviour in terms of action occurrences and the causal relationships between them, but abstract from any auxiliary structure. A configuration structure can also be considered logically, as a class of propositional models, or - equivalently - as a propositional theory in disjunctive normal from. Converting this theory to conjunctive normal form is the key idea in the translation of such a structure into a net. For a variety of classes of event structures we characterise the associated classes of configuration structures in terms of their closure properties, as well as in terms of the axiomatisability of the associated propositional theories by formulae of simple prescribed forms, and in terms of structural properties of the associated Petri nets.

Abstract:
In this paper we deal with additional control structures for decorated PT Nets. The main contribution are inhibitor arcs and priorities. The first ensure that a marking can inhibit the firing of a transition. Inhibitor arcs force that the transition may only fire when the place is empty. an order of transitions restrict the firing, so that an transition may fire only if it has the highest priority of all enabled transitions. This concept is shown to be compatible with reconfigurable Petri nets.

Abstract:
We introduce the concepts of fuzzy Petri nets and marked fuzzy Petri nets along with their appropriate morphisms, which leads to two categories of such Petri nets. Some aspects of the internal structures of these categories are then explored, for example, their reflectiveness/coreflectiveness and symmetrical monoidal closed structure. 1. Introduction Petri nets are a well-known model of concurrent systems [1]. A number of authors have been led to the study of the various categories of Petri nets and their appropriate morphisms [2–4], in the belief that the categorical study provides a tool to compare different models of Petri nets. At the same time, fuzzy Petri nets have also been studied by many authors in different ways [5, 6]. In this paper, taking a cue from [3], we introduce another concept of fuzzy Petri nets (although we model our definition on the lines of [2]). This, along with their appropriate morphisms, results in a category of fuzzy Petri nets (and also of marked fuzzy Petri nets). The structure of these categories is then studied on the lines similar to those in [2], showing that one of the categories is symmetric monoidal closed. 2. Category of Fuzzy Petri Nets For categorical concepts used here, [7] may be referred. We begin by collecting some basic definitions. A Petri net is a bipartite graph, consisting of two kinds of nodes, namely, places and transitions, where arcs are either from a place to a transition or vice versa [3]. Graphically, the places are represented by circles, transitions by rectangles, and the arcs by arrows. We define a fuzzy Petri net as follows. Definition 1. A fuzzy Petri net (in short, fPn) is 4-tuple , where and are sets, called the set of places and set of transitions, respectively, and , are functions, called the incidence functions. We may interpret and defined above as follows. For (resp., ) gives, the grade with which place is related to transition (resp., transition is related to place ). Thus, and describe some kind of fuzzy arcs between places and transitions. Definition 2. An fPn-morphism from an fPn to fPn is a pair of functions, and such that the following two diagrams: (1) “hold”, by which it is meant that for all and . Remark 3. Fuzzy Petri nets and fPn-morphisms form a category, denoted as FPN (the identity morphisms and the composition for this category are obvious to guess). Definition 4. The product of two fPn's and is the fPn , where and are given by for all and . Proposition 5. Let , be the two projections and let , be the two injections. Then , are fPn-morphisms. Proof. To prove that is an

Abstract:
Petri nets are a general and well-established model of concurrent and distributed computation and behaviour, including that taking place in biological systems. In this survey paper, we are concerned with intrinsic relationships between Petri nets and two formal models inspired by aspects of the functioning of the living cell: membrane systems and reaction systems. In particular, we are interested in the benefits that can result from establishing strong semantical links between Petri nets and membrane systems and reaction systems. We first discuss Petri nets with localities reflecting the compartmentalisation modelled in membrane systems. Then special attention is given to set-nets, a new Petri net model for reaction systems and their qualitative approach to the investigation of the processes carried out by biochemical reactions taking place in the living cell.

Abstract:
We introduce {\omega}-Petri nets ({\omega}PN), an extension of plain Petri nets with {\omega}-labeled input and output arcs, that is well-suited to analyse parametric concurrent systems with dynamic thread creation. Most techniques (such as the Karp and Miller tree or the Rackoff technique) that have been proposed in the setting of plain Petri nets do not apply directly to {\omega}PN because {\omega}PN define transition systems that have infinite branching. This motivates a thorough analysis of the computational aspects of {\omega}PN. We show that an {\omega}PN can be turned into an plain Petri net that allows to recover the reachability set of the {\omega}PN, but that does not preserve termination. This yields complexity bounds for the reachability, (place) boundedness and coverability problems on {\omega}PN. We provide a practical algorithm to compute a coverability set of the {\omega}PN and to decide termination by adapting the classical Karp and Miller tree construction. We also adapt the Rackoff technique to {\omega}PN, to obtain the exact complexity of the termination problem. Finally, we consider the extension of {\omega}PN with reset and transfer arcs, and show how this extension impacts the decidability and complexity of the aforementioned problems.

Abstract:
Petri Nets (PNs) are an effective structure
for modeling and analyzing asynchronous systems with concurrent and parallel
activities. A Petri net models the static properties of a discrete event system
concentrating on two basic concepts: events and conditions. Most of the
theoretical work on Petri nets is a formal definition of Petri nets structures,
which consist of a set of places, representing conditions, a set of
transitions, representing events, an input function and an output function. For
practical purposes, a graphical representation is more useful. Two types of
nodes portray places and transitions. A circle is a place and a bar is a
transition. There is no inherent measure of time in a classical Petri net. To
approach time-based evaluation of system performances, Timed Petri Nets (TPNs)
were introduced. Modeling the notion of time is not straightforward. There are
several possibilities for introducing time in PNs, among them timed transitions
and timed places. This paper reviews several published examples where Petri Nets
were used in different circumstances such as estimating expected utilization of
processing resources at steady state in open queueing networks, verifying
computerized simulations and batch planning in textile industry.

Abstract:
We formalise a general concept of distributed systems as sequential components interacting asynchronously. We define a corresponding class of Petri nets, called LSGA nets, and precisely characterise those system specifications which can be implemented as LSGA nets up to branching ST-bisimilarity with explicit divergence.

Abstract:
A Petri net is structurally cyclic if every configuration is reachable from itself in one or more steps. We show that structural cyclicity is decidable in deterministic polynomial time. For this, we adapt the Kosaraju's approach for the general reachability problem for Petri nets.

Abstract:
This study introduces transition vectors based on place transitive matrix derived from graph theory, to study the structure of Petri nets using structure theoretical results that exists in Petri net theory. It has been established that transition vectors provide a simplified and more adequate approach than transitive matrix towards the structural analysis of PN. Some structural classes of Petri nets have been decided and basic concepts about the structure of Petri net have been derived through novel idea of transition vectors. Firstly new representation of place transitive matrix has been introduced for acyclic Petri nets. Secondly Petri net structure has been analyzed and an algorithm to find a directed cycle has been presented with a simplified representation, using transition vectors. Thirdly transition vectors have efficiently been used to identify the particular structures of Petri nets. Finally, useful concepts relevant to the structure of Petri nets have been derived.