Related papers: Coverability, Termination, and Finiteness in Recur…
Petri nets are a classical model of concurrency widely used and studied in formal verification with many applications in modeling and analyzing hardware and software, data bases, and reactive systems. The reachability problem is central…
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…
We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into…
We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) is empty. Our contribution to solve this long-standing problem which relates, for instance, to the reachability…
We investigate bisimulation equivalence on Petri nets under durational semantics. Our motivation was to verify the conjecture that in durational setting, the bisimulation equivalence checking problem becomes more tractable than in ordinary…
We provide an Ackermannian complexity lower bound for the reachability problem for checking programs, a model equivalent to Petri nets. Moreover in fixed dimension $2d+4$, we show that the problem is $\mathbb{F}_d$-hard. As a direct…
Reversible computation is an unconventional form of computing where any executed sequence of operations can be executed in reverse at any point during computation. It has recently been attracting increasing attention in various research…
In a previous paper we introduced immediate observation Petri nets, a subclass of Petri nets with application domains in distributed protocols (population protocols) and theoretical chemistry (chemical reaction networks). IO nets enjoy many…
We show that the language equivalence problem for regular and context-free commutative grammars is coNEXP-complete. In addition, our lower bound immediately yields further coNEXP-completeness results for equivalence problems for…
Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability…
Plans often change due to changes in the situation or our understanding of the situation. Sometimes, a feasible plan may not even exist, and identifying such infeasibilities is useful to determine when requirements need adjustment. Common…
In many complex systems that can be modeled using Petri nets time can be a very important factor which should be taken into account during creation and analysis of the model. Time data can describe starting moments of some actions or their…
Concurrent programming is used in all large and complex computer systems. However, concurrency errors and system failures (ex: crashes and deadlocks) are common. We find that Petri nets can be used to model concurrent systems and find and…
We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As our main result, we prove that for structurally live conservative nets, the…
We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order and modal languages without labels on transitions or atomic propositions on…
We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable:…
Time-Basic Petri nets, is a powerful formalism for model- ing real-time systems where time constraints are expressed through time functions of marking's time description associated with transition, representing possible firing times. We…
We consider formal verification of recursive programs with resource consumption. We introduce prefix replacement systems with non-negative integer counters which can be incremented and reset to zero as a formal model for such programs. In…
Reversible computation is an unconventional form of computing that extends the standard forward-only mode of computation with the ability to execute a sequence of operations in reverse at any point during computation. As such, in this…
Petri nets proved useful to describe various real-world systems, but many of their properties are very hard to check. To alleviate this difficulty, subclasses are often considered. The class of weighted marked graphs with relaxed place…