Simplifications of the recursion scheme

M. D. Gladstone

doi:10.2307/2272468

Simplifications of the recursion scheme

Journal of Symbolic Logic ◽

10.2307/2272468 ◽

1971 ◽

Vol 36 (4) ◽

pp. 653-665 ◽

Cited By ~ 21

Author(s):

M. D. Gladstone

Keyword(s):

Recursion Scheme ◽

Projection Functions ◽

Primitive Recursive

This paper resolves 3 problems left open by R. M. Robinson in [3].We recall that the set of primitive recursive functions is the closure under (i) substitution (or “composition”), and (ii) recursion, of the set P consisting of the zero, successor and projection functions (see any textbook, for instance p. 120 of [2]).

Download Full-text

A reduction of the recursion scheme

Journal of Symbolic Logic ◽

10.2307/2270177 ◽

1968 ◽

Vol 32 (4) ◽

pp. 505-508 ◽

Cited By ~ 12

Author(s):

M. D. Gladstone

Keyword(s):

Recursive Functions ◽

Standard Work ◽

Recursion Scheme ◽

Primitive Recursive

The class of primitive recursive functions may be defined as the closure of certain initial functions, namely the zero, successor and identity functions, under two schemes, namely composition (sometimes called “substitution”) and recursion. For a detailed definition the reader is referred to any standard work, for instance p. 219 of [2], by Kleene.

Download Full-text

Towards efficient verification of population protocols

Formal Methods in System Design ◽

10.1007/s10703-021-00367-3 ◽

2021 ◽

Author(s):

Michael Blondin ◽

Javier Esparza ◽

Stefan Jaax ◽

Philipp J. Meyer

Keyword(s):

Linear Constraints ◽

Computational Power ◽

High Complexity ◽

Reachability Problem ◽

Population Protocols ◽

Finite State ◽

State Agents ◽

Efficient Verification ◽

Primitive Recursive ◽

Very High

AbstractPopulation 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.

Download Full-text