Model Checking Probabilistic Systems Against Pushdown Specifications

Clemens DubslaffClemens Dubslaff, Christel BaierChristel Baier, Manuela BergManuela Berg

DOI Link

Clemens Dubslaff, Christel Baier, Manuela Berg
Model Checking Probabilistic Systems Against Pushdown Specifications
Information Processing Letters, 112(8--9):320--328, 2012

Details
Bibtex

KurzfassungAbstract
Model checking is a fully automatic verification technique traditionally used to verify finite-state systems against regular specifications. Although regular specifications have been proven to be feasible in practice, many desirable specifications are non-regular. For instance, requirements which involve counting cannot be formalized by regular specifications but using pushdown specifications, i.e., context-free properties represented by pushdown automata. Research on model-checking techniques for pushdown specifications is, however, rare and limited to the verification of non-probabilistic systems. In this paper, we address the probabilistic model-checking problem for systems modeled by discrete-time Markov chains and specifications that are provided by deterministic pushdown automata over infinite words. We first consider finite-state Markov chains and show that the quantitative and qualitative model-checking problem is solvable via a product construction and techniques that are known for the verification of probabilistic pushdown automata. Then, we consider recursive systems modeled by probabilistic pushdown automata with an infinite-state Markov chain semantics. We first show that imposing appropriate compatibility (visibility) restrictions on the synchronizations between the pushdown automaton for the system and the specification, decidability of the probabilistic model-checking problem can be established. Finally we prove that slightly departing from this compatibility assumption leads to the undecidability of the probabilistic model-checking problem, even for qualitative properties specified by deterministic context-free specifications.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{DBB2012,
  author  = {Clemens Dubslaff and Christel Baier and Manuela Berg},
  title   = {Model Checking Probabilistic Systems Against Pushdown
             Specifications},
  journal = {Information Processing Letters},
  volume  = {112},
  number  = {8--9},
  year    = {2012},
  pages   = {320--328},
  doi     = {10.1016/j.ipl.2012.01.006}
}