Eliminating Message Counters in Synchronous Threshold Automata
| Autor: | Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Model checking
050101 languages & linguistics Computer science Semantics (computer science) Pipeline (computing) 05 social sciences 02 engineering and technology Automaton Distributed algorithm Asynchronous communication Encoding (memory) Quantifier elimination 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Algorithm |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030670665 VMCAI |
| DOI: | 10.1007/978-3-030-67067-2_10 |
| Popis: | In previous work, we introduced synchronous threshold automata for the verification of synchronous fault-tolerant distributed algorithms, and presented a verification method based on bounded model checking. Modeling a distributed algorithm by a threshold automaton requires to correctly deal with the semantics for sending and receiving messages based on the fault assumption. This step was done manually so far, and required human ingenuity. Motivated by similar results for asynchronous threshold automata, in this paper we show that one can start from a faithful model of the distributed algorithm that includes the sending and receiving of messages, and then automatically obtain a threshold automaton by applying quantifier elimination on the receive message counters. In this way, we obtain a fully automated verification pipeline. We present an experimental evaluation, discovering a bug in our previous manual encoding. Interestingly, while quantifier elimination in general produces larger threshold automata than the manual encoding, the verification times are comparable and even faster in several cases, allowing us to verify benchmarks that could not be handled before. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|