Model checking concurrent programs with nondeterminism and randomization

Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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üchi automaton Spec, a threshold x ∈ [0, 1], and a concurrent program ℙ, the model checking problem asks if the measure of computations of ℙ 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üchi automata specifications) and contrast it with the complexity under the standard semantics that considers all schedulers.

Original languageEnglish (US)
Title of host publication30th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010
Pages364-375
Number of pages12
DOIs
StatePublished - 2010
Event30th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010 - Chennai, India
Duration: Dec 15 2010Dec 18 2010

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume8
ISSN (Print)1868-8969

Other

Other30th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010
CountryIndia
CityChennai
Period12/15/1012/18/10

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Model checking concurrent programs with nondeterminism and randomization'. Together they form a unique fingerprint.

Cite this