Abstract We consider a stateless ‘amnesiac’ variant of the stateful distributed network flooding algorithm, expanding on our conference papers [PODC’19, STACS’20]. Flooding begins with a set of source ‘initial’ nodesIseeking to broadcast a messageMin rounds, in a network represented by an undirected graph (G, E) with set of nodesGand edgesE. In every round, nodes withMsendMto all neighbours from which they did not receiveMin the previous round. Nodes do not remember earlier rounds, raising the possibility thatMcirculates indefinitely. Stateful flooding overcomes this by nodes recording every message circulated and ignoringMif received again. This overhead was assumed to be necessary. We show that almost optimal broadcast can still be achieved without this overhead. We prove that amnesiac flooding terminates on every finite graph and derive sharp bounds for termination times. Define (G, E) to beI-bipartiteif the quotient graph, contracting all nodes inIto a single node, is bipartite. We prove that, ifdis the diameter ande(I) the eccentricity of the setI, flooding terminates ine(I) rounds if (G, E) is I-bipartite andjrounds withe(I)

Flooding is among the simplest and most fundamental of all graph/network algorithms. Consider a (distributed network in the form of a) finite undirected graph G with a distinguished node v that begins flooding by sending copies of the same message to all its neighbours and the neighbours, in the next round, forward the message to all and only the neighbours they did not receive the message from in that round and so on. We assume that nodes do not keep a record of the flooding event, thus, raising the possibility that messages may circulate infinitely even on a finite graph. We call this history-less process amnesiac flooding (to distinguish from a classic distributed implementation of flooding that maintains a history of received messages to ensure a node never sends the same message again). Flooding will terminate when no node in G sends a message in a round, and, thus, subsequent rounds. As far as we know, the question of termination for amnesiac flooding has not been settled - rather, non-termination is implicitly assumed. In this paper, we show that surprisingly synchronous amnesiac flooding always terminates on any arbitrary finite graph and derive exact termination times which differ sharply in bipartite and non-bipartite graphs. In particular, synchronous flooding terminates in e rounds, where e is the eccentricity of the source node, if and only if G is bipartite, and, otherwise, in j rounds where e < j ≤ e+d+1 and d is the diameter of G. Since e is bounded above by d, this implies termination times of at most d and of at most 2d + 1 for bipartite and non-bipartite graphs respectively. This suggests that if communication/broadcast to all nodes is the motivation, the history-less amnesiac flooding is asymptotically time optimal and obviates the need for construction and maintenance of spanning structures like spanning trees. Moreover, the clear separation in the termination times of bipartite and non-bipartite graphs may suggest possible mechanisms for distributed discovery of the topology/distances in an arbitrary graph. For comparison, we also show that, for asynchronous networks, however, an adversary can force the process to be non-terminating.

Flooding is a fundamental distributed algorithms technique. Consider the following flooding process, for simplicity, in a synchronous message passing network: A distinguished node begins the flooding process by sending the (same) message to all its neighbours in the first round. In subsequent rounds, every node receiving the message relays a copy of the message further to all those, and only those, nodes it did not receive the message from in the previous round. However, the nodes do not remember if they've taken part in the flooding before and therefore will repeat the process every time they get a message. In other words, they execute an amnesiac flooding process with memory only of the present round. The flooding process terminates in a particular round when no edge in the network carries the message in that, and, hence, subsequent, rounds. We call this process Amnesiac Flooding (AF).

We extend the monodic fragment of first-order linear temporal logic to include right-linear grammar operators and quantification of propositional variables. Unlike propositional temporal logic, the use of grammar operators in first-order temporal logic is not equivalent to general propositional quantification, as the latter admit satisfiable formulae without countable models. We consider the decision problem for fragments where propositional quantification occurs outside of quantification of individual variables and temporal (grammar) operators. We show that if externally quantified propositions inside temporal operators occur within positive occurrences of universal quantifiers for individual variables, then validity for all propositional prefix classes is recursively enumerable and decidable in the two-variable case. Without this condition we show that, even with very severe restrictions on the first-order part of the logic, no non-trivial prefix class is recursively enumerable.

Abstract We present a concrete version of Astesiano and Zucca's CCS/PC, that permits parametric channels of a special form which are used in prefix expressions and in an extended way in relabelling functions. We report on the use of the calculus to describe nested process context in a parallel operating system.

The authors report on the use of formal methods for the development of parallel operating systems for two experimental declarative systems over a five-year period. A common specification approach has evolved as part of the development of these two very different systems: one being for a parallel graph reduction machine and written in a functional language enhanced with state-based objects, the other was written in C/sup ++/. A brief overview of each system is given before concentrating on the use of formal methods. A description is given of how both a technique for formally specifying sequential systems (VDM) and a technique for specifying concurrent systems (temporal logic) have been used together. In both cases, the issue of verification is addressed.>