DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2018.20

Selective Monitoring

Authors: Radu Grigore and Stefan Kiefer

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract

We study selective monitors for labelled Markov chains. Monitors observe the outputs that are generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty. A monitor is selective if it skips observations in order to reduce monitoring overhead. We are interested in monitors that minimize the expected number of observations. We establish an undecidability result for selectively monitoring general Markov chains. On the other hand, we show for non-hidden Markov chains (where any output identifies the state the Markov chain is in) that simple optimal monitors exist and can be computed efficiently, based on DFA language equivalence. These monitors do not depend on the precise transition probabilities in the Markov chain. We report on experiments where we compute these monitors for several open-source Java projects.

Cite as

Radu Grigore and Stefan Kiefer. Selective Monitoring. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 20:1-20:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{grigore_et_al:LIPIcs.CONCUR.2018.20,
  author =	{Grigore, Radu and Kiefer, Stefan},
  title =	{{Selective Monitoring}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{20:1--20:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.20},
  URN =		{urn:nbn:de:0030-drops-95586},
  doi =		{10.4230/LIPIcs.CONCUR.2018.20},
  annote =	{Keywords: runtime monitoring, probabilistic systems, Markov chains, automata, language equivalence}
}

Document

DOI: 10.4230/LIPIcs.ICALP.2016.104

Proving the Herman-Protocol Conjecture

Authors: Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, and James Worrell

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract

Herman's self-stabilization algorithm, introduced 25 years ago, is a well-studied synchronous randomized protocol for enabling a ring of N processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilization is the central outstanding open problem about this protocol. It is known that there is a constant h such that any initial configuration has expected stabilization time at most hN2. Ten years ago, McIver and Morgan established a lower bound of 4/27 ~ 0.148 for h, achieved with three equally-spaced tokens, and conjectured this to be the optimal value of h. A series of papers over the last decade gradually reduced the upper bound on h, with the present record (achieved in 2014) standing at approximately 0.156. In this paper, we prove McIver and Morgan's conjecture and establish that h = 4/27 is indeed optimal.

Cite as

Maria Bruna, Radu Grigore, Stefan Kiefer, Joël Ouaknine, and James Worrell. Proving the Herman-Protocol Conjecture. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 104:1-104:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bruna_et_al:LIPIcs.ICALP.2016.104,
  author =	{Bruna, Maria and Grigore, Radu and Kiefer, Stefan and Ouaknine, Jo\"{e}l and Worrell, James},
  title =	{{Proving the Herman-Protocol Conjecture}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{104:1--104:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.104},
  URN =		{urn:nbn:de:0030-drops-62393},
  doi =		{10.4230/LIPIcs.ICALP.2016.104},
  annote =	{Keywords: randomized protocols, self-stabilization, Lyapunov function, expected time}
}

Search Results

Documents authored by Grigore, Radu

Selective Monitoring

Abstract

Cite as

Proving the Herman-Protocol Conjecture

Abstract

Cite as

Thanks for your feedback!

Could not send message