International Center for Computational Logic - Benutzerbeiträge [de]

Inproceedings3442

2025-10-30T16:39:29Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
|To appear=0
|Year=2025
|Month=August
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, QEST+FORMATS 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings
|Pages=195--218
|Publisher=Springer
|Editor=Pavithra Prabhaka, Andrea Vandin
|Series=Lecture Notes in Computer Science
|Volume=16143
}}
{{Publikation Details
|Link=https://doi.org/10.1007/978-3-032-05792-1_11
|DOI Name=10.1007/978-3-032-05792-1_11
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3443

2025-10-30T16:38:01Z

Patrick Wienhöft: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Carlos E. |ErsterAutorNachname=Budde |FurtherAuthors=Arnd Hartmanns; Tobias Meggendorfer; Maximilian Weininger; Patrick Wienhöft }} {{Inproceedings |Referiert=1 |Title=Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality |To appear=0 |Year=2025 |Month=August |Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint…“

{{Publikation Erster Autor
|ErsterAutorVorname=Carlos E.
|ErsterAutorNachname=Budde
|FurtherAuthors=Arnd Hartmanns; Tobias Meggendorfer; Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality
|To appear=0
|Year=2025
|Month=August
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, QEST+FORMATS 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings
|Pages=83--94
|Publisher=Springer
|Editor=Pavithra Prabhaka, Andrea Vandin
|Series=Lecture Notes in Computer Science
|Volume=16143
}}
{{Publikation Details
|Link=https://doi.org/10.1007/978-3-032-05792-1_5
|DOI Name=10.1007/978-3-032-05792-1_5
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3442

2025-10-30T16:35:12Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
|To appear=0
|Year=2025
|Month=August
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, {QEST+FORMATS} 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings
|Pages=195--218
|Publisher=Springer
|Editor=Pavithra Prabhaka, Andrea Vandin
|Series=Lecture Notes in Computer Science
|Volume=16143
}}
{{Publikation Details
|Link=https://doi.org/10.1007/978-3-032-05792-1_11
|DOI Name=10.1007/978-3-032-05792-1_11
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3442

2025-10-30T16:34:03Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
|To appear=0
|Year=2025
|Month=August
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, {QEST+FORMATS} 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings
|Pages=195--218
|Publisher=Springer
|Editor=Pavithra Prabhaka, Andrea Vandin
|Series=Lecture Notes in Computer Science
|Volume=16143
}}
{{Publikation Details
|Link=https://doi.org/10.1007/978-3-032-05792-1_11
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3442

2025-10-30T16:32:00Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
|To appear=0
|Year=2025
|Month=August
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, {QEST+FORMATS} 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings
|Pages=195--218
|Publisher=Springer
|Editor=Pavithra Prabhaka, Andrea Vandin
|Series=Lecture Notes in Computer Science
|Volume=16143
}}
{{Publikation Details
|Link=https://doi.org/10.1007/978-3-032-05792-1_11
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3442

2025-10-30T16:31:40Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
|To appear=0
|Year=2025
|Month=August
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, {QEST+FORMATS} 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings
|Pages=195--218
|Publisher=Springer
|Editor=Pavithra Prabhaka, Andrea Vandin
|Series=Lecture Notes in Computer Science
|Volume=16143
}}
{{Publikation Details
|Link=https://doi.org/10.1007/978-3-032-05792-1_11
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
|BibTex=@inproceedings{DBLP:conf/qestformats/MeggendorferWW25,
author = {Tobias Meggendorfer and
Maximilian Weininger and
Patrick Wienh{\"{o
}}

Inproceedings3442

2025-10-30T16:31:05Z

Patrick Wienhöft: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Tobias |ErsterAutorNachname=Meggendorfer |FurtherAuthors=Maximilian Weininger; Patrick Wienhöft }} {{Inproceedings |Referiert=1 |Title=What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes |To appear=0 |Year=2025 |Month=August |Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference…“

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
|To appear=0
|Year=2025
|Month=August
|Booktitle=Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems - Second International Joint Conference, {QEST+FORMATS} 2025, Aarhus, Denmark, August 26-28, 2025, Proceedings
|Pages=195--218
|Publisher=Springer
|Editor=Pavithra Prabhaka, Andrea Vandin
|Series=Lecture Notes in Computer Science
|Volume=16143
}}
{{Publikation Details
|Link=https://doi.org/10.1007/978-3-032-05792-1_11
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
|BibTex=@inproceedings{DBLP:conf/qestformats/MeggendorferWW25,
author = {Tobias Meggendorfer and
Maximilian Weininger and
Patrick Wienh{\"{o}}ft},
editor = {Pavithra Prabhakar and
Andrea Vandin},
title = {What Are the Odds? Improving Statistical Model Checking of Markov
Decision Processes},
booktitle = {Quantitative Evaluation of Systems and Formal Modeling and Analysis
of Timed Systems - Second International Joint Conference, {QEST+FORMATS}
2025, Aarhus, Denmark, August 26-28, 2025, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {16143},
pages = {195--218},
publisher = {Springer},
year = {2025},
doi = {10.1007/978-3-032-05792-1\_11}
}
}}

Inproceedings3406

2025-05-05T11:47:56Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=Solving Robust Markov Decision Processes: Generic, Reliable, Efficient
|To appear=0
|Year=2025
|Month=April
|Booktitle=Proceedings of the 39th Annual AAAI Conference on Artificial Intelligence
|Pages=26631-26641
|Publisher=AAAI Press
|Editor=Toby Walsh, Julie Shah, Zico Kolter
|Series=25
|Volume=39
}}
{{Publikation Details
|Abstract=Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities.
In *robust* MDP (RMDP), every action is associated with an *uncertainty set* of probability distributions, modelling that transition probabilities are not known precisely.
Based on the known theoretical connection to stochastic games, we provide a framework for solving RMDPs that is generic, reliable, and efficient.
It is *generic* both with respect to the model, allowing for a wide range of uncertainty sets, including but not limited to intervals, L1- or L2-balls, and polytopes; and with respect to the objective, including long-run average reward, undiscounted total reward, and stochastic shortest path.
It is *reliable*, as our approach not only converges in the limit, but provides precision guarantees at any time during the computation.
It is *efficient* because -- in contrast to state-of-the-art approaches -- it avoids explicitly constructing the underlying stochastic game.
Consequently, our prototype implementation outperforms existing tools by several orders of magnitude and can solve RMDPs with a million states in under a minute.
|ISBN=978-1-57735-897-8
|ISSN=2159-5399
|Download=34865-Article Text-38932-1-2-20250410-1.pdf
|DOI Name=10.1609/AAAI.V39I25.34865
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3407

2025-05-05T11:47:17Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Caros E.
|ErsterAutorNachname=Budde
|FurtherAuthors=Arnd Hartmanns; Tobias Meggendorfer; Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=Sound Statistical Model Checking for Probabilities and Expected Rewards
|To appear=0
|Year=2025
|Booktitle=LNCS
|Pages=167-190
|Publisher=Springer Nature Switzerland
|Editor=Arie Gurfinkel, Marijn Heule
|Volume=15696
}}
{{Publikation Details
|Abstract=Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.
|ISSN=1611-3349
|Link=https://link.springer.com/chapter/10.1007/978-3-031-90643-5_9
|DOI Name=10.1007/978-3-031-90643-5_9
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3407

2025-05-02T14:50:02Z

Patrick Wienhöft:

{{Publikation Erster Autor
|ErsterAutorVorname=Caros E.
|ErsterAutorNachname=Budde
|FurtherAuthors=Arnd Hartmanns; Tobias Meggendorfer; Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=Sound Statistical Model Checking for Probabilities and Expected Rewards
|To appear=0
|Year=2025
|Booktitle=LNCS
|Pages=167-190
|Publisher=Springer Nature Switzerland
|Editor=Arie Gurfinkel, Marijn Heule
|Volume=15696
}}
{{Publikation Details
|Abstract=Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.
|ISSN=1611-3349
|Link=https://link.springer.com/chapter/10.1007/978-3-031-90643-5_9
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Inproceedings3407/en

2025-05-02T14:47:15Z

Patrick Wienhöft: Page created automatically by parser function on page Inproceedings3407

#REDIRECT [[Inproceedings3407]]

Inproceedings3407

2025-05-02T14:47:15Z

Patrick Wienhöft: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Caros E. |ErsterAutorNachname=Budde |FurtherAuthors=Arnd Hartmanns; Tobias Meggendorfer; Maximilian Weininger; Patrick Wienhöft }} {{Inproceedings |Referiert=1 |Title=Sound Statistical Model Checking for Probabilities and Expected Rewards |To appear=0 |Year=2025 |Booktitle=LNCS |Pages=167-190 |Publisher=Springer |Editor=Arie Gurfinkel, Marijn Heule |Volume=15696 }} {{Publikation Details |ISSN=1611-3349 |Link…“

Inproceedings3406/en

2025-04-29T08:04:43Z

Patrick Wienhöft: Page created automatically by parser function on page Inproceedings3406

#REDIRECT [[Inproceedings3406]]

Inproceedings3406

2025-04-29T08:04:42Z

Patrick Wienhöft: Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Tobias |ErsterAutorNachname=Meggendorfer |FurtherAuthors=Maximilian Weininger; Patrick Wienhöft }} {{Inproceedings |Referiert=1 |Title=Solving Robust Markov Decision Processes: Generic, Reliable, Efficient |To appear=0 |Year=2025 |Month=April |Booktitle=Proceedings of the 39th Annual AAAI Conference on Artificial Intelligence |Pages=26631-26641 |Publisher=AAAI Press |Editor=Toby Walsh, Julie Shah, Zico Kolte…“

{{Publikation Erster Autor
|ErsterAutorVorname=Tobias
|ErsterAutorNachname=Meggendorfer
|FurtherAuthors=Maximilian Weininger; Patrick Wienhöft
}}
{{Inproceedings
|Referiert=1
|Title=Solving Robust Markov Decision Processes: Generic, Reliable, Efficient
|To appear=0
|Year=2025
|Month=April
|Booktitle=Proceedings of the 39th Annual AAAI Conference on Artificial Intelligence
|Pages=26631-26641
|Publisher=AAAI Press
|Editor=Toby Walsh, Julie Shah, Zico Kolter
|Series=25
|Volume=39
}}
{{Publikation Details
|Abstract=Markov decision processes (MDP) are a well-established model for sequential decision-making in the presence of probabilities.
In *robust* MDP (RMDP), every action is associated with an *uncertainty set* of probability distributions, modelling that transition probabilities are not known precisely.
Based on the known theoretical connection to stochastic games, we provide a framework for solving RMDPs that is generic, reliable, and efficient.
It is *generic* both with respect to the model, allowing for a wide range of uncertainty sets, including but not limited to intervals, L1- or L2-balls, and polytopes; and with respect to the objective, including long-run average reward, undiscounted total reward, and stochastic shortest path.
It is *reliable*, as our approach not only converges in the limit, but provides precision guarantees at any time during the computation.
It is *efficient* because -- in contrast to state-of-the-art approaches -- it avoids explicitly constructing the underlying stochastic game.
Consequently, our prototype implementation outperforms existing tools by several orders of magnitude and can solve RMDPs with a million states in under a minute.
|ISBN=978-1-57735-897-8
|ISSN=2159-5399
|Download=34865-Article Text-38932-1-2-20250410-1.pdf
|Projekt=CPEC, CeTI
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}

Datei:34865-Article Text-38932-1-2-20250410-1.pdf

2025-04-29T08:04:01Z

Patrick Wienhöft: