arXiv subjects

Kittiphon Phalakarn

Publications and source records attributed to Kittiphon Phalakarn.

8 recordsLinked to original sources

arXiv2026

Value Iteration for Stochastic Parity Games

We present the first (bounded) value iteration algorithm for the quantitative analysis of stochastic parity games, a fundamental model for probabilistic verification with $ω$-regular objectives. Existing algorithms are based on strategy iteration, which repeatedly computes optimal strategies for one player while fixing the other, leading to high computational cost. Our value iteration algorithm instead operates directly on a lattice-theoretic characterization of winning probabilities, exploiting structural properties of (almost-sure qualitative) winning states under parity objectives. We prove correctness and convergence of the proposed algorithm.

cs.GT↗

arXiv2026

A Coalgebraic Dijkstra Algorithm

The Dijkstra algorithm is a classical method for solving the shortest path problem on weighted graphs. There are several variations of the Dijkstra algorithm, including algorithms for the widest path problem and for two-player games. In this paper, we introduce the coalgebraic shortest path problem (CSPP), a unifying framework for a broad class of optimization problems on state-transition systems. This framework encompasses not only the aforementioned problems but also new ones such as the shortest binary tree problem. We further present a coalgebraic Dijkstra algorithm for solving the CSPP efficiently under a suitable condition. Our condition is necessary and sufficient for the algorithm to return correct solutions, thereby providing a precise criterion for when Dijkstra-style acceleration is possible. We also show that the proposed algorithm achieves asymptotic complexity comparable to that of the classical Dijkstra algorithm.

cs.DS↗

arXiv2025

Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control

Stochastic games are fundamental in various applications, including the control of cyber-physical systems (CPS), where both controller and environment are modeled as players. Traditional algorithms typically aim to determine a single winning strategy to develop a controller. However, in CPS control and other domains, permissive controllers are essential, as they enable the system to adapt when additional constraints arise and remain resilient to runtime changes. This work generalizes the concept of (permissive winning) strategy templates, originally introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to incorporate stochastic games. These templates capture an infinite number of winning strategies, allowing for efficient strategy adaptation to system changes. We focus on two winning criteria (almost-sure and positive winning) and five winning objectives (safety, reachability, Büchi, co-Büchi, and parity). Our contributions include algorithms for constructing templates for each winning criterion and objective and a novel approach for extracting a winning strategy from a given template. Discussions on comparisons between templates and between strategy extraction methods are provided.

eess.SY↗

arXiv2025

A Matrix Decomposition Method for Odd-Type Gaussian Normal Basis Multiplication

Normal basis is used in many applications because of the efficiency of the implementation. However, most space complexity reduction techniques for binary field multiplier are applicable for only optimal normal basis or Gaussian normal basis of even type. There are 187 binary fields GF(2^k) for k from 2 to 1,000 that use odd-type Gaussian normal basis. This paper presents a method to reduce the space complexity of odd-type Gaussian normal basis multipliers over binary field GF(2^k). The idea is adapted from the matrix decomposition method for optimal normal basis. The result shows that our space complexity reduction method can reduce the number of XOR gates used in the implementation comparing to previous works with a small trade-off in critical path delay.

cs.AR↗

arXiv2025

Optimal Representation for Right-to-Left Parallel Scalar Point Multiplication

This paper introduces an optimal representation for a right-to-left parallel elliptic curve scalar point multiplication. The right-to-left approach is easier to parallelize than the conventional left-to-right approach. However, unlike the left-to-right approach, there is still no work considering number representations for the right-to-left parallel calculation. By simplifying the implementation by Robert, we devise a mathematical model to capture the computation time of the calculation. Then, for any arbitrary amount of doubling time and addition time, we propose algorithms to generate representations which minimize the time in that model. As a result, we can show a negative result that a conventional representation like NAF is almost optimal. The parallel computation time obtained from any representation cannot be better than NAF by more than 1%.

cs.DM↗

arXiv2025

Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games

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.

cs.LO↗

arXiv2025

Chance and Mass Interpretations of Probabilities in Markov Decision Processes (Extended Version)

Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over sequences of states and with schedulers making random choices. An alternative view, especially well-suited for modeling dynamical systems, defines MDPs as distribution transformers with schedulers distributing probability masses. Our main contribution is a unified semantical framework that accommodates these two views and two new ones. These four semantics of MDPs arise naturally through identifying different sources of randomness in an MDP (namely schedulers, configurations, and transitions) and providing different ways of interpreting these probabilities (called the chance and mass interpretations). These semantics are systematically unified through a mathematical construct called chance-mass (CM) classifier. As another main contribution, we study a reachability problem in each of the two new semantics, demonstrating their hardness and providing two algorithms for solving them.

cs.FL↗

arXiv2020

Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games

Solving stochastic games with the reachability objective is a fundamental problem, especially in quantitative verification and synthesis. For this purpose, bounded value iteration (BVI) attracts attention as an efficient iterative method. However, BVI's performance is often impeded by costly end component (EC) computation that is needed to ensure convergence. Our contribution is a novel BVI algorithm that conducts, in addition to local propagation by the Bellman update that is typical of BVI, global propagation of upper bounds that is not hindered by ECs. To conduct global propagation in a computationally tractable manner, we construct a weighted graph and solve the widest path problem in it. Our experiments show the algorithm's performance advantage over the previous BVI algorithms that rely on EC computation.

cs.LO↗