Complexity of Verification and Synthesis of Threshold Automata

A. R. Balasubramanian, Javier Esparza, Marijana Lazić

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

Abstract

Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct the first systematic study of the complexity of verification and synthesis problems for threshold automata. We prove that the coverability, reachability, safety, and liveness problems are NP-complete, and that the bounded synthesis problem is complete. A key to our results is a novel characterization of the reachability relation of a threshold automaton as an existential Presburger formula. The characterization also leads to novel verification and synthesis algorithms. We report on an implementation, and provide experimental results.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
EditorsDang Van Hung, Oleg Sokolsky
PublisherSpringer Science and Business Media Deutschland GmbH
Pages144-160
Number of pages17
ISBN (Print)9783030591519
DOIs
StatePublished - 2020
Event18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 - Hanoi, Viet Nam
Duration: 19 Oct 202023 Oct 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12302 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
Country/TerritoryViet Nam
CityHanoi
Period19/10/2023/10/20

Keywords

  • Distributed algorithms
  • Parameterized verification
  • Threshold automata

Fingerprint

Dive into the research topics of 'Complexity of Verification and Synthesis of Threshold Automata'. Together they form a unique fingerprint.

Cite this