Model Checking Concurrent Programs with Nondeterminism and Randomization

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

• Type: Journal
• Year: 2010
• Where: FSTTCS
• Authors: Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan
• Keywords: Checking, FSTTCS 2010, Model, Probabilistic Programs, Software Engineering