Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems

We introduce the notion of a validating labelled state transition and message production system (VLSM), a tool for formal modeling and analysing faulty distributed systems. The central focus of our investigation is equivocation, a faulty behaviour that we formally model, reason about, and then show how to detect from durable evidence that may be available locally to system components. Equivocating components exhibit behaviour that is inconsistent with single-trace system executions, while also only interacting with other components by sending and receiving valid messages. Components of system are called validators for that system if their validity constraints validate that the messages they receive are producible by the system. Our main result shows that for systems of validators, the effect that Byzantine components can have on honest nodes is precisely identical to the effect that equivocating validators can have on non-equivocating validators. Therefore, for distributed systems of potentially faulty validators, replacing Byzantine nodes with equivocating validators has no material analytical consequences, and forms the basis of a sound alternative foundation to Byzantine fault tolerance analysis.