DROPS

Document

Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)

Authors: Swen Jacobs, Kenneth McMillan, Roopsha Samanta, and Ilya Sergey

Published in: Dagstuhl Reports, Volume 13, Issue 3 (2023)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 23112 "Unifying Formal Methods for Trustworthy Distributed Systems". Distributed systems are challenging to develop and reason about. Unsurprisingly, there have been many efforts in formally specifying, modeling, and verifying distributed systems. A bird’s eye view of this vast body of work reveals two primary sensibilities. The first is that of semi-automated or interactive deductive verification targeting structured programs and implementations, and focusing on simplifying the user’s task of providing inductive invariants. The second is that of fully-automated model checking, targeting more abstract models of distributed systems, and focusing on extending the boundaries of decidability for the parameterized model checking problem. Regrettably, solution frameworks and results in deductive verification and parameterized model checking have largely evolved in isolation while targeting the same overall goal. This seminar aimed at enabling conversations and solutions cutting across the deductive verification and model checking communities, leveraging the complementary strengths of these approaches. In particular, we explored layered and compositional approaches for modeling and verification of industrial-scale distributed systems that lend themselves well to separation of verification tasks, and thereby the use of diverse proof methodologies.

Cite as

Swen Jacobs, Kenneth McMillan, Roopsha Samanta, and Ilya Sergey. Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112). In Dagstuhl Reports, Volume 13, Issue 3, pp. 32-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{jacobs_et_al:DagRep.13.3.32,
  author =	{Jacobs, Swen and McMillan, Kenneth and Samanta, Roopsha and Sergey, Ilya},
  title =	{{Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)}},
  pages =	{32--48},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{13},
  number =	{3},
  editor =	{Jacobs, Swen and McMillan, Kenneth and Samanta, Roopsha and Sergey, Ilya},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.3.32},
  URN =		{urn:nbn:de:0030-drops-192278},
  doi =		{10.4230/DagRep.13.3.32},
  annote =	{Keywords: Deductive Verification, Distributed Algorithms, Formal Verification, Model Checking}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2014.431

Lipschitz Robustness of Finite-state Transducers

Authors: Thomas A. Henzinger, Jan Otop, and Roopsha Samanta

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

Abstract

We investigate the problem of checking if a finite-state transducer is robust to uncertainty in its input. Our notion of robustness is based on the analytic notion of Lipschitz continuity - a transducer is K-(Lipschitz) robust if the perturbation in its output is at most K times the perturbation in its input. We quantify input and output perturbation using similarity functions. We show that K-robustness is undecidable even for deterministic transducers. We identify a class of functional transducers, which admits a polynomial time automata-theoretic decision procedure for K-robustness. This class includes Mealy machines and functional letter-to-letter transducers. We also study K-robustness of nondeterministic transducers. Since a nondeterministic transducer generates a set of output words for each input word, we quantify output perturbation using set-similarity functions. We show that K-robustness of nondeterministic transducers is undecidable, even for letter-to-letter transducers. We identify a class of set-similarity functions which admit decidable K-robustness of letter-to-letter transducers.

Cite as

Thomas A. Henzinger, Jan Otop, and Roopsha Samanta. Lipschitz Robustness of Finite-state Transducers. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 431-443, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.FSTTCS.2014.431,
  author =	{Henzinger, Thomas A. and Otop, Jan and Samanta, Roopsha},
  title =	{{Lipschitz Robustness of Finite-state Transducers}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{431--443},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.431},
  URN =		{urn:nbn:de:0030-drops-48614},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.431},
  annote =	{Keywords: Robustness, Transducers, Weighted Automata}
}

Search Results

Documents authored by Samanta, Roopsha

Unifying Formal Methods for Trustworthy Distributed Systems (Dagstuhl Seminar 23112)

Abstract

Cite as

Lipschitz Robustness of Finite-state Transducers

Abstract

Cite as

Thanks for your feedback!

Could not send message