Semantisches Browsen
Aus International Center for Computational Logic
The automata-based model checking approach … The automata-based model checking approach for randomized distributed systems relies on an operational interleaving semantics of the system by means of a Markov decision process and a formalization of the desired event E by an ω-regular linear-time property, e.g., an LTL formula. The task is then to compute the greatest lower bound for the probability for E that can be guaranteed even in worst-case scenarios. Such bounds can be computed by a combination of polynomially time-bounded graph algorithm with methods for solving linear programs. In the classical approach, the “worst-case” is determined when ranging over all schedulers that decide which action to perform next. In particular, all possible interleavings and resolutions of other nondeterministic choices in the system model are taken into account. The worst-case analysis relying on this general notion of schedulers is often too pessimistic and leads to extreme probability values that can be achieved only by schedulers that are unrealistic for parallel systems. This motivates the switch to more realistic classes of schedulers that respect the fact that the individual processes only have partial information about the global system states. Such classes of partial-information schedulers yield more realistic worst-case probabilities, but computationally they are much harder. A wide range of verification problems turns out to be undecidable when the goal is to check that certain probability bounds hold under all partial-information schedulers. under all partial-information schedulers. +
@inproceedings{B2010,
author = {Christel Baier},
title = {On model checking techniques for randomized distributed systems},
booktitle = {Proc. of the 8th International Conference on Integrated Formal
Methods (IFM)},
series = {Lecture Notes in Computer Science},
volume = {6396},
publisher = {Springer},
year = {2010},
pages = {1--11},
doi = {10.1007/978-3-642-16265-7_1}
}
author = {Christel Baier},
title = {On model checking techniques for randomized distributed systems},
booktitle = {Proc. of the 8th International Conference on Integrated Formal
Methods (IFM)},
series = {Lecture Notes in Computer Science},
volume = {6396},
publisher = {Springer},
year = {2010},
pages = {1--11},
doi = {10.1007/978-3-642-16265-7_1}
}
Baier +
Christel +
Christel Baier<br/> '''[[Inproceedings1595539574|<b>On model checking techniques for randomized distributed systems</b>]] … Christel Baier<br/> '''[[Inproceedings1595539574|<b>On model checking techniques for randomized distributed systems</b>]]''' <br/>__NOTOC__<i>Proc. of the 8th International Conference on Integrated Formal Methods (IFM)</i>, volume 6396 of Lecture Notes in Computer Science, 1--11, 2010. Springer<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Inproceedings1595539574|Details]]ceedings1595539574|Details]] +
Christel Baier<br/> '''[[Inproceedings1595539574/en|<b>On model checking techniques for randomized distributed systems</b>]] … Christel Baier<br/> '''[[Inproceedings1595539574/en|<b>On model checking techniques for randomized distributed systems</b>]]''' <br/>__NOTOC__<i>Proc. of the 8th International Conference on Integrated Formal Methods (IFM)</i>, volume 6396 of Lecture Notes in Computer Science, 1--11, 2010. Springer<br/><span class="fas fa-chevron-right" style="font-size: 85%;" ></span> [[Inproceedings1595539574|Details]]ceedings1595539574|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.
On model checking techniques for randomized distributed systems +
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:40:13 +
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.
On model checking techniques for randomized distributed systems +, On model checking techniques for randomized distributed systems +, On model checking techniques for randomized distributed systems +, On model checking techniques for randomized distributed systems + und On model checking techniques for randomized distributed systems +
