Coverability, Termination, and Finiteness in Recursive Petri Nets

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.

Computable embeddability for algebraic structures

In computability theory, the standard tool to classify preorders is provided by the computable reducibility. If [Formula: see text] and [Formula: see text] are preorders with domain [Formula: see text], then [Formula: see text] is computably reducible to [Formula: see text] if and only if there is a computable function [Formula: see text] such that for all [Formula: see text] and [Formula: see text], [Formula: see text] [Formula: see text][Formula: see text]. We study the complexity of preorders which arise in a natural way in computable structure theory. We prove that the relation of computable isomorphic embeddability among computable torsion abelian groups is a [Formula: see text] complete preorder. A similar result is obtained for computable distributive lattices. We show that the relation of primitive recursive embeddability among punctual structures (in the setting of Kalimullin et al.) is a [Formula: see text] complete preorder.

Definitional schemes for primitive recursive and computable functions

The unary primitive recursive functions can be defined in terms of a finite set of initial functions together with a finite set of unary and binary operations that are primitive recursive in their inputs. We reduce arity considerations, by show that two fixed unary operations suffice, and a single initial function can be chosen arbitrarily. The method works for many other classes of functions, including the unary partial computable functions. For this class of partial functions we also show that a single unary operation (together with any finite set of initial functions) will never suffice.

Arithmetic Formulated in a Logic of Meaning Containment

We assess Meyer’s formalization of arithmetic in his [21], based on the strong relevant logic R and compare this with arithmetic based on a suitable logic of meaning containment, which was developed in Brady [7]. We argue in favour of the latter as it better captures the key logical concepts of meaning and truth in arithmetic. We also contrast the two approaches to classical recapture, again favouring our approach in [7]. We then consider our previous development of Peano arithmetic including primitive recursive functions, finally extending this work to that of general recursion.

Towards efficient verification of population protocols

Population protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is -hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class $${ WS}^3$$ WS 3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that $${ WS}^3$$ WS 3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership and correctness problems for $${ WS}^3$$ WS 3 reduce to solving boolean combinations of linear constraints over $${\mathbb {N}}$$ N . This allowed us to develop the first software able to automatically prove correctness for all of the infinitely many possible inputs.

The Decidability of Verification under PS 2.0

We consider the reachability problem for finite-state multi-threaded programs under thepromising semantics() of Lee et al., which captures most common program transformations. Since reachability is already known to be undecidable in the fragment of with only release-acquire accesses (-), we consider the fragment with only relaxed accesses and promises (). We show that reachability under is undecidable in general and that it becomes decidable, albeit non-primitive recursive, if we bound the number of promises.Given these results, we consider a bounded version of the reachability problem. To this end, we bound both the number of promises and of “view-switches”, i.e., the number of times the processes may switch their local views of the global memory. We provide a code-to-code translation from an input program under (with relaxed and release-acquire memory accesses along with promises) to a program under SC, thereby reducing the bounded reachability problem under to the bounded context-switching problem under SC. We have implemented a tool and tested it on a set of benchmarks, demonstrating that typical bugs in programs can be found with a small bound.