Specification of Synchronous Network Flooding in Temporal Logic

摘要

In distributed network algorithms, network flooding is considered one of the simplest and most fundamental algorithms. This research specifies the basic synchronous memory-less network flooding algorithm where nodes on the network don't have memory, for any fixed size of network, in Linear Temporal Logic. The specification can be customized to any single network topology or class of topologies. A specification of the termination problem is formulated and used to compare different topologies for earlier termination. This paper gives a worked example of one topology resulting in earlier termination than another, for which we perform a formal verification using the model checker NuSMV.