License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2010.364
URN: urn:nbn:de:0030-drops-28788
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2878/
Go to the corresponding LIPIcs Volume Portal

Chadha, Rohit ; Sistla, A. Prasad ; Viswanathan, Mahesh

Model Checking Concurrent Programs with Nondeterminism and Randomization

pdf-format:
32.pdf (0.5 MB)

Abstract

For concurrent probabilistic programs having process-level nondeterminism, it is often necessary to restrict the class of schedulers that resolve nondeterminism to obtain sound and precise model checking algorithms. In this paper, we introduce two classes of schedulers called view consistent and locally Markovian schedulers and consider the model checking problem of concurrent, probabilistic programs under these alternate semantics. Specifically, given a B\"{u}chi automaton $Spec$, a threshold $x$ in $[0,1]$, and a concurrent program $P$, the model checking problem asks if the measure of computations of $P$ that satisfy $Spec$ is at least $x$, under all view consistent (or locally Markovian) schedulers. We give precise complexity results for the model checking problem (for different classes of B\"{u}chi automata specifications) and contrast it with the complexity under the standard semantics that considers all schedulers.

BibTeX - Entry

@InProceedings{chadha_et_al:LIPIcs:2010:2878,
  author =	{Rohit Chadha and A. Prasad Sistla and Mahesh Viswanathan},
  title =	{{Model Checking Concurrent Programs with Nondeterminism and  Randomization}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{364--375},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Kamal Lodaya and Meena Mahajan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2878},
  URN =		{urn:nbn:de:0030-drops-28788},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.364},
  annote =	{Keywords: view consistent scheduler, locally Markovian scheduler, model-checking, probabilistic program}
}

Keywords: view consistent scheduler, locally Markovian scheduler, model-checking, probabilistic program
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)
Issue Date: 2010
Date of publication: 14.12.2010

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