Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCoverability, Termination, and Finiteness in Recursive Petri Nets
121
0
0.0
(
0
)
Added by
Igor Khmelnitsky
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic 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.
rate research
Read More
We consider approaches for causal semantics of Petri nets, explicitly representing dependencies between transition occurrences. For one-safe nets or condition/event-systems, the notion of process as defined by Carl Adam Petri provides a notion of a run of a system where causal dependencies are reflected in terms of a partial order. A well-known problem is how to generalise this notion for nets where places may carry several tokens. Goltz and Reisig have defined such a generalisation by distinguishing tokens according to their causal history. However, this so-called individual token interpretation is often considered too detailed. A number of approaches have tackled the problem of defining a more abstract notion of process, thereby obtaining a so-called collective token interpretation. Here we give a short overview on these attempts and then identify a subclass of Petri nets, called structural conflict nets, where the interplay between conflict and concurrency due to token multiplicity does not occur. For this subclass, we define abstract processes as equivalence classes of Goltz-Reisig processes. We justify this approach by showing that we obtain exactly one maximal abstract process if and only if the underlying net is conflict-free with respect to a canonical notion of conflict.
We prove that $omega$-languages of (non-deterministic) Petri nets and $omega$-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of $omega$-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of $omega$-languages of (non-deterministic) Turing machines which also form the class of effective analytic sets. In particular, for each non-null recursive ordinal $alpha < omega_1^{{rm CK}} $ there exist some ${bf Sigma}^0_alpha$-complete and some ${bf Pi}^0_alpha$-complete $omega$-languages of Petri nets, and the supremum of the set of Borel ranks of $omega$-languages of Petri nets is the ordinal $gamma_2^1$, which is strictly greater than the first non-recursive ordinal $omega_1^{{rm CK}}$. We also prove that there are some ${bf Sigma}_1^1$-complete, hence non-Borel, $omega$-languages of Petri nets, and that it is consistent with ZFC that there exist some $omega$-languages of Petri nets which are neither Borel nor ${bf Sigma}_1^1$-complete. This answers the question of the topological complexity of $omega$-languages of (non-deterministic) Petri nets which was left open in [DFR14,FS14].
The categorical modeling of Petri nets has received much attention recently. The Dialectica construction has also had its fair share of attention. We revisit the use of the Dialectica construction as a categorical model for Petri nets generalizing the original application to suggest that Petri nets with different kinds of transitions can be modeled in the same categorical framework. Transitions representing truth-values, probabilities, rates or multiplicities, evaluated in different algebraic structures called lineales are useful and are modeled here in the same category. We investigate (categorical instances of) this generalized model and its connections to more recent models of categorical nets.
Due to the mobility and frequent disconnections, the correctness of mobile interaction systems, such as mobile robot systems and mobile payment systems, are often difficult to analyze. This paper introduces three critical properties of systems, called system connectivity, interaction soundness and data validity, and presents a related modeling and analysis method, based on a kind of Petri nets called VPN. For a given system, a model including component nets and interaction structure nets is constructed by using VPNs. The component net describes the internal process of each component, while the interaction structure net reflects the dynamic interaction between components. Based on this model, three properties are defined and analyzed. The case study of a practical mobile payment system shows the effectiveness of the proposed method.
We develop a polynomial translation from finite control pi-calculus processes to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural in that there is a close correspondence between the control flows, enjoys a bisimulation result, and is suitable for practical model checking.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
