TY - GEN
T1 - Model checking concurrent programs with nondeterminism and randomization
AU - Chadha, Rohit
AU - Prasad Sistla, A.
AU - Viswanathan, Mahesh
N1 - The assistance of Mr T. J. Lynch and his staff in field work is very much appreciated. This research formed part of the author's PhD study at the Pastoral Science Group, Massey University. We thank the New Zealand Ministry of Foreign Affairs and Trade, the Consejo Nacional de Ciencia y Tecnologia (CONACYT, Mexico), and the Colegio de Postgraduados (Mexico) for provision of post-graduate stipend and financial assistance.
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84867159913
UR - https://www.scopus.com/pages/publications/84867159913#tab=citedBy
U2 - 10.4230/LIPIcs.FSTTCS.2010.364
DO - 10.4230/LIPIcs.FSTTCS.2010.364
M3 - Conference contribution
AN - SCOPUS:84867159913
SN - 9783939897231
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 364
EP - 375
BT - 30th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010
T2 - 30th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010
Y2 - 15 December 2010 through 18 December 2010
ER -