NDLI: Model Checking of Recursive Probabilistic Systems

Please wait, while we are loading the content...

Model Checking of Recursive Probabilistic Systems

Content Provider	ACM Digital Library
Author	Yannakakis, Mihalis Etessami, Kousha
Copyright Year	2012
Abstract	Recursive Markov Chains (RMCs) are a natural abstract model of procedural probabilistic programs and related systems involving recursion and probability. They succinctly define a class of denumerable Markov chains that generalize several other stochastic models, and they are equivalent in a precise sense to probabilistic Pushdown Systems. In this article, we study the problem of model checking an RMC against an $\textit{ω}-regular$ specification, given in terms of a Büchi automaton or a Linear Temporal Logic (LTL) formula. Namely, given an RMC $\textit{A}$ and a property, we wish to know the probability that an execution of $\textit{A}$ satisfies the property. We establish a number of strong upper bounds, as well as lower bounds, both for $\textit{qualitative}$ problems (is the probability = 1, or = 0?), and for $\textit{quantitative}$ problems (is the probability $≥ \textit{p}?,$ or, approximate the probability to within a desired precision). The complexity upper bounds we obtain for automata and LTL properties are similar, although the algorithms are different. We present algorithms for the qualitative model checking problem that run in polynomial space in the size $\|\textit{A}\|$ of the RMC and exponential time in the size of the property (the automaton or the LTL formula). For several classes of RMCs, including single-exit RMCs (a class that encompasses some well-studied stochastic models, for instance, stochastic context-free grammars) the algorithm runs in polynomial time in $\|\textit{A}\|.$ For the quantitative model checking problem, we present algorithms that run in polynomial space in the RMC and exponential space in the property. For the class of linearly recursive RMCs we can compute the exact probability in time polynomial in the RMC and exponential in the property. For deterministic automata specifications, all our complexities in the specification come down by one exponential. For lower bounds, we show that the qualitative model checking problem, even for a fixed RMC, is already EXPTIME-complete. On the other hand, even for simple reachability analysis, we know from our prior work that our PSPACE upper bounds in $\textit{A}$ can not be improved substantially without a breakthrough on a well-known open problem in the complexity of numerical computation.
Starting Page	1
Ending Page	40
Page Count	40
File Format	PDF
ISSN	15293785
e-ISSN	1557945X
DOI	10.1145/2159531.2159534
Volume Number	13
Issue Number	2
Journal	ACM Transactions on Computational Logic (TOCL)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2012-04-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Büchi automata Markov chains Model checking Probabilistic systems Pushdown systems Recursive systems Stochastic context-free grammars Temporal logic
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Logic Computational Mathematics Computer Science

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Model checking stochastic automata

Translating to Co-Büchi Made Tight, Unified, and Useful

Checking timed Büchi automata emptiness on simulation graphs

Analysis of recursive state machines

Analyzing probabilistic pushdown automata

Checking LTL properties of recursive Markov chains

Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems

Tool support for learning Büchi automata and linear temporal logic

Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations

Model Checking of Recursive Probabilistic Systems

Similar Documents

Model checking stochastic automata

Translating to Co-Büchi Made Tight, Unified, and Useful

Checking timed Büchi automata emptiness on simulation graphs

Analysis of recursive state machines

Analyzing probabilistic pushdown automata

Checking LTL properties of recursive Markov chains

Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems

Tool support for learning Büchi automata and linear temporal logic

Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations

Model Checking of Recursive Probabilistic Systems