Modelling Message Protocols for the Byzantine Generals Problem with PrT-Nets

摘要

The Byzantine Generals Problem requires the nonfaulty processors of a distributed network to agree upon a value even though the faulty components may interfere in a malicious way. Different algorithms for reaching agreement have been presented. In the paper, basic solutions using oral messages and authenticated messages are modelled and studied with the help of predicate/transition nets. Message system models are introduced for the single Generals case, for the case of concurrent single Generals and also for the case of general consensus. The S-invariants of the nets have been determined and system properties like liveness, synchronization and consistency have been studied with net-theoretical methods.