ATVA 2025
Mon 27 - Fri 31 October 2025 Bengaluru, India

This program is tentative and subject to change.

Wed 29 Oct 2025 12:00 - 12:30 at R102 - Games Chair(s): Sayan Mukherjee

For model checking stochastic games (SGs), bounded value iteration (BVI) algorithms have gained attention as efficient approximate methods with rigorous precision guarantees. However, BVI may not terminate or converge when the target SG contains end components. Most existing approaches address this issue by explicitly detecting and processing end components—a process that is often computationally expensive. An exception is the widest path-based BVI approach previously studied by Phalakarn et al., which we refer to as 1WP-BVI. The method performs particularly well in the presence of numerous end components. Nonetheless, its theoretical foundations remain somewhat ad hoc. In this paper, we identify and formalize the core principles underlying the widest path-based BVI approach by (i) presenting 2WP-BVI, a clean BVI algorithm based on (2-player) widest path games, and (ii) proving its correctness using what we call the maximality inheritance principle—a proof principle previously employed in a well-known result in probabilistic model checking. Our experimental results demonstrate the practical relevance and potential of our proposed 2WP-BVI algorithm.

This program is tentative and subject to change.

Wed 29 Oct

Displayed time zone: Chennai, Kolkata, Mumbai, New Delhi change

11:00 - 12:30
GamesATVA Papers at R102
Chair(s): Sayan Mukherjee Univ Rennes, Inria, CNRS, IRISA, France
11:00
30m
Paper
Energy Games with Weight Uncertainty
ATVA Papers
Orna Kupferman Hebrew University, Naama Shamash Halevy The Hebrew University
11:30
30m
Paper
Quantitative Strategy Templates
ATVA Papers
Ashwani Anand Max Planck Institute for Software Systems, Satya Prakash Nayak Max Planck Institute for Software Systems (MPI-SWS), Ritam Raha University of Antwerp, Antwerp, Belgium, Irmak Saglam Max Planck Institute for Software Systems (MPI-SWS), Anne-Kathrin Schmuck Max Planck Institute for Software Systems
12:00
30m
Paper
Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games
ATVA Papers
Kittiphon Phalakarn National Institute of Informatics, Yun Chen Tsai National Institute of Informatics, Japan, Ichiro Hasuo National Institute of Informatics, Japan
Hide past events