2 Search Results for "Aiswarya, Cyriac"

Document
DOI: 10.4230/LIPIcs.CONCUR.2015.340
An Automata-Theoretic Approach to the Verification of Distributed Algorithms

Authors: Cyriac Aiswarya, Benedikt Bollig, and Paul Gastin

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

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.
Cite as

Cyriac Aiswarya, Benedikt Bollig, and Paul Gastin. An Automata-Theoretic Approach to the Verification of Distributed Algorithms. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 340-353, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{aiswarya_et_al:LIPIcs.CONCUR.2015.340,
  author =	{Aiswarya, Cyriac and Bollig, Benedikt and Gastin, Paul},
  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 =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.340},
  URN =		{urn:nbn:de:0030-drops-53737},
  doi =		{10.4230/LIPIcs.CONCUR.2015.340},
  annote =	{Keywords: distributed algorithms, verification, leader election}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2014.11
Reasoning About Distributed Systems: WYSIWYG (Invited Talk)

Authors: Aiswarya Cyriac and Paul Gastin

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
There are two schools of thought on reasoning about distributed systems: one following interleaving based semantics, and one following partial-order/graph based semantics. This paper compares these two approaches and argues in favour of the latter. An introductory treatment of the split-width technique is also provided.
Cite as

Aiswarya Cyriac and Paul Gastin. Reasoning About Distributed Systems: WYSIWYG (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 11-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{cyriac_et_al:LIPIcs.FSTTCS.2014.11,
  author =	{Cyriac, Aiswarya and Gastin, Paul},
  title =	{{Reasoning About Distributed Systems: WYSIWYG}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{11--30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.11},
  URN =		{urn:nbn:de:0030-drops-48283},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.11},
  annote =	{Keywords: Verification of distributed systems, Communicating recursive programs, Partial order/graph semantics, Split-width and tree interpretation}
}
  • Refine by Author
  • 2 Gastin, Paul
  • 1 Aiswarya, Cyriac
  • 1 Bollig, Benedikt
  • 1 Cyriac, Aiswarya

  • Refine by Classification

  • Refine by Keyword
  • 1 Communicating recursive programs
  • 1 Partial order/graph semantics
  • 1 Split-width and tree interpretation
  • 1 Verification of distributed systems
  • 1 distributed algorithms
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2014
  • 1 2015

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact