Inproceedings1383849030: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christel |ErsterAutorNachname=Baier }} {{Inproceedings |Booktitle=Proc. of the 5th International Conference on Algebraic Informatics (CAI) |Pages=4--5 |Publisher=Springer |Series=Lecture Notes in Computer Science |Title=Quantitative Analysis of Randomized Distributed Systems and Probabilistic Automata |Volume=8080 |Year=2013 }} {{Publikation Details |DOI Name=10.1007/978-3-642-40663-8_2 |Abstra…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 15: | Zeile 15: | ||
|DOI Name=10.1007/978-3-642-40663-8_2 | |DOI Name=10.1007/978-3-642-40663-8_2 | ||
|Abstract=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 (MDP) 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. | |Abstract=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 (MDP) 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. | ||
|Forschungsgruppe= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 15:41 Uhr
Quantitative Analysis of Randomized Distributed Systems and Probabilistic Automata
Christel BaierChristel Baier
Christel Baier
Quantitative Analysis of Randomized Distributed Systems and Probabilistic Automata
Proc. of the 5th International Conference on Algebraic Informatics (CAI), volume 8080 of Lecture Notes in Computer Science, 4--5, 2013. Springer
Quantitative Analysis of Randomized Distributed Systems and Probabilistic Automata
Proc. of the 5th International Conference on Algebraic Informatics (CAI), volume 8080 of Lecture Notes in Computer Science, 4--5, 2013. Springer
- KurzfassungAbstract
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 (MDP) 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. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@inproceedings{B2013,
author = {Christel Baier},
title = {Quantitative Analysis of Randomized Distributed Systems and
Probabilistic Automata},
booktitle = {Proc. of the 5th International Conference on Algebraic
Informatics (CAI)},
series = {Lecture Notes in Computer Science},
volume = {8080},
publisher = {Springer},
year = {2013},
pages = {4--5},
doi = {10.1007/978-3-642-40663-8_2}
}
