Semantisches Browsen
Aus International Center for Computational Logic
Model checking is a fully automatic verifi … 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.deterministic context-free specifications. +
@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}
}
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}
}
Dubslaff +
Clemens +
Clemens Dubslaff, Christel Baier, Manuela … Clemens Dubslaff, Christel Baier, Manuela Berg<br/> '''[[Article1106562267|Model Checking Probabilistic Systems Against Pushdown Specifications]]''' <br/>__NOTOC__Information Processing Letters, 112(8--9):320--328, 2012<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Article1106562267|Details]]ticle1106562267|Details]] +
Clemens Dubslaff, Christel Baier, Manuela … Clemens Dubslaff, Christel Baier, Manuela Berg<br/> '''[[Article1106562267/en|Model Checking Probabilistic Systems Against Pushdown Specifications]]''' <br/>__NOTOC__Information Processing Letters, 112(8--9):320--328, 2012<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Article1106562267|Details]]ticle1106562267|Details]] +
Anzeigetitel„Anzeigetitel <span style="font-size:small;">(Display title of)</span>“ ist ein softwareseitig fest definiertes Attribut, das einen eindeutigen Anzeigetitel zu einem Objekt speichert und ihm zuweist. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Model Checking Probabilistic Systems Against Pushdown Specifications +
Zuletzt geändert„Zuletzt geändert <span style="font-size:small;">(Modification date)</span>“ ist ein softwareseitig fest definiertes Attribut, das das Datum der letzten Änderung einer Seite speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
5. März 2025, 13:42:07 +
Hat Abfrage„Hat Abfrage <span style="font-size:small;">(Has query)</span>“ ist ein softwareseitig fest definiertes Attribut, das die Metainformationen einer Abfrage als <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">Subobjekt</a> speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Model Checking Probabilistic Systems Against Pushdown Specifications +, Model Checking Probabilistic Systems Against Pushdown Specifications +, Model Checking Probabilistic Systems Against Pushdown Specifications +, Model Checking Probabilistic Systems Against Pushdown Specifications +, Model Checking Probabilistic Systems Against Pushdown Specifications +, Model Checking Probabilistic Systems Against Pushdown Specifications + und Model Checking Probabilistic Systems Against Pushdown Specifications +
