License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.340
URN: urn:nbn:de:0030-drops-53737
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5373/
Go to the corresponding LIPIcs Volume Portal

Aiswarya, Cyriac ; Bollig, Benedikt ; Gastin, Paul

An Automata-Theoretic Approach to the Verification of Distributed Algorithms

pdf-format:
13.pdf (1 MB)

Abstract

We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, each round allowing a process to perform a bounded sequence of actions such as send or receive a pid, store it in some register, and compare register contents wrt. the associated total order. An algorithm is supposed to be correct independently of the number of processes. To specify correctness properties, we introduce a logic that can reason about processes and pids. Referring to leader election, it may say that, at the end of an execution, each process stores the maximum pid in some dedicated register. Since the verification of distributed algorithms is undecidable, we propose an underapproximation technique, which bounds the number of rounds. This is an appealing approach, as the number of rounds needed by a distributed algorithm to conclude is often exponentially smaller than the number of processes. We provide an automata-theoretic solution, reducing model checking to emptiness for alternating two-way automata on words. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete.

BibTeX - Entry

@InProceedings{aiswarya_et_al:LIPIcs:2015:5373,
  author =	{Cyriac Aiswarya and Benedikt Bollig and Paul Gastin},
  title =	{{An Automata-Theoretic Approach to the Verification of Distributed Algorithms}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{340--353},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Luca Aceto and David de Frutos Escrig},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5373},
  URN =		{urn:nbn:de:0030-drops-53737},
  doi =		{10.4230/LIPIcs.CONCUR.2015.340},
  annote =	{Keywords: distributed algorithms, verification, leader election}
}

Keywords: distributed algorithms, verification, leader election
Collection: 26th International Conference on Concurrency Theory (CONCUR 2015)
Issue Date: 2015
Date of publication: 26.08.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI