<div class="csl-bib-body">
<div class="csl-entry">Stoilkovska, I., Konnov, I., Widder, J., & Zuleger, F. (2020). Eliminating Message Counters in Threshold Automata. In <i>Automated Technology for Verification and Analysis. 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings</i> (pp. 192–212). Springer. https://doi.org/10.34726/423</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/16503
-
dc.identifier.uri
https://doi.org/10.34726/423
-
dc.description.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).
en
dc.description.sponsorship
Austrian Science Fund (FWF)
-
dc.description.sponsorship
Austrian Science Fund (FWF)
-
dc.description.sponsorship
Austrian Science Fund (FWF)
-
dc.description.sponsorship
Interchain Foundation, Switzerland
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
distributed algorithms
en
dc.subject
fault tolerance
en
dc.subject
modeling
en
dc.subject
threshold automata
en
dc.subject
abstraction
en
dc.subject
quantifier elimination
en
dc.title
Eliminating Message Counters in Threshold Automata
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Urheberrechtsschutz
de
dc.rights.license
In Copyright
en
dc.identifier.doi
10.34726/423
-
dc.relation.isbn
978-3-030-59152-6
-
dc.relation.doi
10.1007/978-3-030-59152-6
-
dc.description.startpage
192
-
dc.description.endpage
212
-
dc.relation.grantno
S11403
-
dc.relation.grantno
S11405
-
dc.relation.grantno
W1255
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Automated Technology for Verification and Analysis. 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings
-
tuw.container.volume
12302
-
tuw.peerreviewed
true
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.version
am
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
tuw.publisher.doi
10.1007/978-3-030-59152-6_11
-
dc.identifier.libraryid
AC17205157
-
dc.description.numberOfPages
21
-
tuw.author.orcid
0000-0003-1468-8398
-
dc.rights.identifier
Urheberrechtsschutz
de
dc.rights.identifier
In Copyright
en
tuw.relation.issn
0302-9743
-
tuw.relation.eissn
1611-3349
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
open
-
item.fulltext
with Fulltext
-
item.openairetype
conference paper
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E191-02 - Forschungsbereich Embedded Computing Systems
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering