Equational calculus for primitive recursive rational-valued functions

M. Kh. Fakhmi

doi:10.1007/bf01084087

Equational calculus for primitive recursive rational-valued functions

Journal of Soviet Mathematics ◽

10.1007/bf01084087 ◽

1976 ◽

Vol 6 (4) ◽

pp. 444-448

Author(s):

M. Kh. Fakhmi

Keyword(s):

Equational Calculus ◽

Primitive Recursive

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

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