اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCoverability, Termination, and Finiteness in Recursive Petri Nets
121
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
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.
قيم البحث
اقرأ أيضاً
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 r
un 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-determinist
ic) 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 th
e 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, calle
d 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.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
