Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDialectica Petri nets
118
0
0.0
(
0
)
Added by
Wilmer Leal
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
Petri networks and network models are two frameworks for the compositional design of systems of interacting entities. Here we show how to combine them using the concept of a catalyst: an entity that is neither destroyed nor created by any process it engages in. In a Petri net, a place is a catalyst if its in-degree equals its out-degree for every transition. We show how a Petri net with a chosen set of catalysts gives a network model. This network model maps any list of catalysts from the chosen set to the category whose morphisms are all the processes enabled by this list of catalysts. Applying the Grothendieck construction, we obtain a category fibered over the category whose objects are lists of catalysts. This category has as morphisms all processes enabled by some list of catalysts. While this category has a symmetric monoidal structure that describes doing processes in parallel, its fibers also have premonoidal structures that describe doing one process and then another while reusing the catalysts.
We study detectability properties for labeled Petri nets and finite automata. We first study weak approximate detectability (WAD) that implies that there exists an infinite observed output sequence of the system such that each prefix of the output sequence with length greater than a given value allows an observer to determine if the current state belongs to a given set. We also consider two new concepts called instant strong detectability (ISD) and eventual strong detectability (ESD). The former property implies that for each possible infinite observed output sequence each prefix of the output sequence allows reconstructing the current state. The latter implies that for each possible infinite observed output sequence, there exists a value such that each prefix of the output sequence with length greater than that value allows reconstructing the current state. Results: WAD: undecidable for labeled Petri nets, PSPACE-complete for finite automata ISD: decidable and EXPSPACE-hard for labeled Petri nets, belongs to P for finite automata ESD: decidable under promptness assumption and EXPSPACE-hard for labeled Petri nets, belongs to P for finite automata SD: belongs to P for finite automata, strengthens Shu and Lins 2011 results based on two assumptions of deadlock-freeness and promptness ISD<SD<ESD<WD<WAD for both labeled Petri nets and finite automata
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and the currently best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from LICS 2019. We establish a non-elementary lower bound, i.e. that the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi and other areas, that are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the currently best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack.
Godels Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theoretic transformations (so-called proof interpretations) that are based on Godels Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on Godel fibrations, we present a (hyper)doctrine characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that we derive in the category theory the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra. This requires extra logical principles, going beyond intuitionistic logic, Markovs Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. This tight correspondence should come handy not only when discussing the applications of the Dialectica already known, like its use to extract computational content from (some) classical theorems (proof mining), its use to help to model specific abstract machines, etc. but also to help devise new applications.
This paper proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimax basis reachability graph (minimax-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net is blocking. We prove that a bounded deadlock-free Petri net is nonblocking if and only if its minimax-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the minimax-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of deadlock markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the minimax-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
