Title: Eliminating Message Counters in Threshold Automata
Authors: Stoilkovska, Ilina 
Konnov, Igor 
Widder, Josef 
Zuleger, Florian 
Keywords: distributed algorithms; fault tolerance; modeling; threshold automata; abstraction; quantifier elimination
Issue Date: 12-Oct-2020
Book Title: Automated Technology for Verification and Analysis. 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings 
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. LTL-X properties (satisfied by all our benchmarks).
URI: http://hdl.handle.net/20.500.12708/16503
http://dx.doi.org/10.34726/423
DOI: 10.34726/423
Organisation: E192 - Institut für Logic and Computation 
License: Urheberrechtsschutz 1.0
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:

File Description SizeFormat Existing users please Login
main.pdf408.18 kBAdobe PDFEmbargoed until October 13, 2021    Request a copy
Show full item record

Page view(s)

42
checked on Feb 26, 2021

Download(s)

16
checked on Feb 26, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.