Anzeige
Erschienen in:
2020 | OriginalPaper | Buchkapitel
Eliminating Message Counters in Threshold Automata
verfasst von : Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger
Erschienen in: Automated Technology for Verification and Analysis
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
Threshold automata were introduced to give a formal semantics to distributed algorithms in a way that supports automated verification. While transitions in threshold automata are guarded by conditions over the number of globally sent messages, conditions in the pseudocode descriptions of distributed algorithms are usually formulated over the number of locally received messages. In this work, we provide an automated method to close the gap between these two representations. We propose threshold automata with guards over the number of received messages and present abstractions into guards over the number of sent messages, by eliminating the receive message counters. Our approach allows us for the first time to fully automatically verify models of distributed algorithms that are in one-to-one correspondence with their pseudocode. We prove that our method is sound, and present a criterion for completeness w.r.t. \({\mathsf {LTL}}_{\text {-}\mathsf {{X}}}\) properties (satisfied by all our benchmarks).