Zobrazeno 1 - 10
of 62
pro vyhledávání: '"KAMINSKI, BENJAMIN LUCIEN"'
Markov decision processes (MDPs) with rewards are a widespread and well-studied model for systems that make both probabilistic and nondeterministic choices. A fundamental result about MDPs is that their minimal and maximal expected rewards satisfy Be
Externí odkaz:
http://arxiv.org/abs/2411.16564
We study Hoare-like logics, including partial and total correctness Hoare logic, incorrectness logic, Lisbon logic, and many others through the lens of predicate transformers \`a la Dijkstra and through the lens of Kleene algebra with top and tests (
Externí odkaz:
http://arxiv.org/abs/2411.06416
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing calculi allow reasoning about the expected value that a quantity assumes
Externí odkaz:
http://arxiv.org/abs/2404.05097
Autor:
Schröer, Philipp, Batz, Kevin, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Matheja, Christoph
This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (IV
Externí odkaz:
http://arxiv.org/abs/2309.07781
This report contains the proceedings of the 19th International Workshop on Termination (WST 2023), which was held in Obergurgl during August 24--25 as part of Obergurgl Summer on Rewriting (OSR 2023).
Externí odkaz:
http://arxiv.org/abs/2308.09536
Autor:
Feng, Shenghua, Chen, Mingshuai, Su, Han, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Zhan, Naijun
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lowe
Externí odkaz:
http://arxiv.org/abs/2302.06082
Autor:
Batz, Kevin, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Matheja, Christoph, Verscht, Lena
We develop a weakest-precondition-style calculus \`a la Dijkstra for reasoning about amortized expected runtimes of randomized algorithms with access to dynamic memory - the $\textsf{aert}$ calculus. Our calculus is truly quantitative, i.e. instead o
Externí odkaz:
http://arxiv.org/abs/2211.12923
Autor:
Batz, Kevin, Chen, Mingshuai, Junges, Sebastian, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Matheja, Christoph
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reac
Externí odkaz:
http://arxiv.org/abs/2205.06152
Autor:
Batz, Kevin, Gallus, Adrian, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Winkler, Tobias
We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs with two additional features: (1) nondeterministic branching and (2)
Externí odkaz:
http://arxiv.org/abs/2202.07577
We present a novel strongest-postcondition-style calculus for quantitative reasoning about non-deterministic programs with loops. Whereas existing quantitative weakest pre allows reasoning about the value of a quantity after a program terminates on a
Externí odkaz:
http://arxiv.org/abs/2202.06765