Stopping Criteria for Value Iteration on Concurrent Stochastic
Reachability and Safety Games

D 2025

Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games

GROBELNA, Marta; Jan KŘETÍNSKÝ a Maximilian WEININGER

Základní údaje

Originální název

Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games

Autoři

GROBELNA, Marta; Jan KŘETÍNSKÝ a Maximilian WEININGER

Vydání

Singapore, Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games, od s. 568-580, 13 s. 2025

Nakladatel

IEEE

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/25:00143631

Organizační jednotka

Fakulta informatiky

ISBN

979-8-3315-7900-5

ISSN

DOI

https://doi.org/10.1109/LICS65433.2025.00049

EID Scopus

2-s2.0-105020013727

Klíčová slova anglicky

Formal methods; foundations of probabilistic systems and games; verification; model checking

Štítky

core_A, firank_1

Změněno: 2. 4. 2026 16:09, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals.VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are ϵ-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are ϵ-close.

Návaznosti

MUNI/I/1757/2021, interní kód MU

Název: MUNI Award in Science and Humanities (Akronym: Křetínský)

Investor: Masarykova univerzita, MUNI Award in Science and Humanities, MASH - MUNI Award in Science and Humanities

Citovat

GROBELNA, Marta; Jan KŘETÍNSKÝ a Maximilian WEININGER. Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games. Online. In Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games. Singapore: IEEE, 2025, s. 568-580. ISBN 979-8-3315-7900-5. Dostupné z: https://doi.org/10.1109/LICS65433.2025.00049.

@inproceedings{2551302,
   author = {Grobelna, Marta and Křetínský, Jan and Weininger, Maximilian},
   address = {Singapore},
   booktitle = {Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games},
   doi = {https://doi.org/10.1109/LICS65433.2025.00049},
   keywords = {Formal methods; foundations of probabilistic systems and games; verification; model checking},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Singapore},
   isbn = {979-8-3315-7900-5},
   pages = {568-580},
   publisher = {IEEE},
   title = {Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games},
   year = {2025}
}

TY  - CONF
ID  - 2551302
AU  - Grobelna, Marta - Křetínský, Jan - Weininger, Maximilian
PY  - 2025
TI  - Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games
PB  - IEEE
CY  - Singapore
SN  - 9798331579005
KW  - Formal methods
KW  - foundations of probabilistic systems and games
KW  - verification
KW  - model checking
N2  - We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals.VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are ϵ-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are ϵ-close.
ER  -

GROBELNA, Marta; Jan KŘETÍNSKÝ a Maximilian WEININGER. Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games. Online. In \textit{Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games}. Singapore: IEEE, 2025, s.~568-580. ISBN~979-8-3315-7900-5. Dostupné z: https://doi.org/10.1109/LICS65433.2025.00049.

Přehled o publikaci