PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP

AGARWAL, Chaitanya; Shibashis GUHA; Jan KŘETÍNSKÝ a Pazhamalai MURUGANANDHAM. PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Springer, 2022, s. 3-25. ISBN 9783031131875. Dostupné z: https://doi.org/10.1007/978-3-031-13188-2_1.

Základní údaje

Originální název

PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP

Autoři

AGARWAL, Chaitanya; Shibashis GUHA; Jan KŘETÍNSKÝ a Pazhamalai MURUGANANDHAM

Vydání

Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II, od s. 3-25, 23 s. 2022

Nakladatel

Springer

---

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Ne

Organizační jednotka

Fakulta informatiky

ISBN

9783031131875

ISSN

DOI

https://doi.org/10.1007/978-3-031-13188-2_1

---

Anotace

V originále

Markov decision processes (MDP) and continuous-time MDP (CTMDP) are the fundamental models for non-deterministic systems with probabilistic uncertainty. Mean payoff (a.k.a. long-run average reward) is one of the most classic objectives considered in their context. We provide the first algorithm to compute mean payoff probably approximately correctly in unknown MDP; further, we extend it to unknown CTMDP. We do not require any knowledge of the state space, only a lower bound on the minimum transition probability, which has been advocated in literature. In addition to providing probably approximately correct (PAC) bounds for our algorithm, we also demonstrate its practical nature by running experiments on standard benchmarks.