arXiv subjects

Ichiro Hasuo

Publications and source records attributed to Ichiro Hasuo.

At least 19 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 $\omega$-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↗

arXiv2026

Monads and Distributive Laws in Substructural Contexts (Extended Version)

We present a categorical theory of monads and distributive laws in substructural contexts. In the study of distributive laws, the roles of (the absence of) structural rules for variable contexts have been recognized; our theory formalizes these substructural situations using Tronin's verbal categories $\mathbf W$, in a uniform and presentation-independent manner. We introduce the classes of $\mathbf W$-operadic monads (those defined via the structural rules in $\mathbf W$) and of $\mathbf W$-commutative monads (those invariant under the structural rules in $\mathbf W$). We give a canonical construction of a distributive law $ST\to TS$ of monads on $\mathbf{Set}$; it is applicable when $S$ is $\mathbf W$-operadic and $T$ is $\mathbf W$-commutative (under mild conditions). This accounts for many known and new distributive laws. Even when $S$ fails to be $\mathbf W$-operadic, we can refine $S$ and force $\mathbf W$-operadicity; this captures Varacca and Winskel's construction of indexed valuations.

cs.LO↗

arXiv2026

Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking

We introduce a hybrid spatiotemporal logic for automotive safety applications (HSTL), focused on highway driving. Spatiotemporal logic features specifications about vehicles throughout space and time, while hybrid logic enables precise references to individual vehicles and their historical positions. We define the semantics of HSTL and provide a baseline model-checking algorithm for it. We propose two optimized model-checking algorithms, which reduce the search space based on the reachable states and possible transitions from one state to another. All three model-checking algorithms are evaluated on a series of common driving scenarios such as safe following, safe crossings, overtaking, and platooning. An exponential performance improvement is observed for the optimized algorithms.

cs.LO↗

arXiv2026

STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version)

Modern cyber-physical systems are complex, and requirements are often written in Signal Temporal Logic (STL). Writing the right STL is difficult in practice; engineers benefit from concrete executions that illustrate what a specification actually admits. Trace synthesis addresses this need, but a single witness rarely suffices to understand intent or explore edge cases - diverse satisfying behaviors are far more informative. We introduce diversified trace synthesis: the automatic generation of sets of behaviorally diverse traces that satisfy a given STL formula. Building on a MILP encoding of STL and system model, we formalize three complementary diversification objectives - Boolean distance, random Boolean distance, and value distance - all captured by an objective function and solved iteratively. We implement these ideas in STLts-Div, a lightweight Python tool that integrates with Gurobi.

eess.SY↗

arXiv2025

A Variety of Request-Response Specifications

We find, motivated by real-world applications, that the well-known request-response specification comes with multiple variations, and that these variations should be distinguished. As the first main contribution, we introduce a classification of those variations into six types, and present it as a decision tree, where a user is led to the type that is suited for their application by answering a couple of questions. Our second main contribution is the formalization of those six types in various formalisms such as temporal logics, grammars, and automata; here, two types out of the six are non-regular specifications and their formalization requires extended formalisms. We also survey tools for monitoring these specifications to cater for practitioners' needs.

cs.FL↗

arXiv2025

Compositional Verification of Almost-Sure B\"uchi Objectives in MDPs

This paper studies the verification of almost-sure B\"uchi objectives in MDPs with a known, compositional structure based on string diagrams. In particular, we ask whether there is a strategy that ensures that a B\"uchi objective is almost-surely satisfied. We first show that proper exit sets -- the sets of exits that can be reached within a component without losing locally -- together with the reachability of a B\"uchi state are a sufficient and necessary statistic for the compositional verification of almost-sure B\"uchi objectives. The number of proper exit sets may grow exponentially in the number of exits. We define two algorithms: (1) A straightforward bottom-up algorithm that computes this statistic in a recursive manner to obtain the verification result of the entire string diagram and (2) a polynomial-time iterative algorithm which avoids computing all proper exit sets by performing iterative strategy refinement.

cs.LO↗

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

Componentwise Automata Learning for System Integration (Extended Version)

Compositional automata learning is attracting attention as an analysis technique for complex black-box systems. It exploits a target system's internal compositional structure to reduce complexity. In this paper, we identify system integration -- the process of building a new system as a composite of potentially third-party and black-box components -- as a new application domain of compositional automata learning. Accordingly, we propose a new problem setting, where the learner has direct access to black-box components. This is in contrast with the usual problem settings of compositional learning, where the target is a legacy black-box system and queries can only be made to the whole system (but not to components). We call our problem componentwise automata learning for distinction. We identify a challenge there called component redundancies: some parts of components may not contribute to system-level behaviors, and learning them incurs unnecessary effort. We introduce a contextual componentwise learning algorithm that systematically removes such redundancies. We experimentally evaluate our proposal and show its practical relevance.

cs.FL↗

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↗

arXiv2024

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\"uchi, co-B\"uchi, 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↗

arXiv2024

Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications

We present a bounded model checking algorithm for signal temporal logic (STL) that exploits mixed-integer linear programming (MILP). A key technical element is our novel MILP encoding of the STL semantics; it follows the idea of stable partitioning from the recent work on SMT-based STL model checking. Assuming that our (continuous-time) system models can be encoded to MILP -- typical examples are rectangular hybrid automata (precisely) and hybrid dynamics with closed-form solutions (approximately) -- our MILP encoding yields an optimization-based model checking algorithm that is scalable, is anytime/interruptible, and accommodates parameter mining. Experimental evaluation shows our algorithm's performance advantages especially for complex STL formulas, demonstrating its practical relevance e.g. in the automotive domain.

eess.SY↗

arXiv2024

A Unifying Approach to Product Constructions for Quantitative Temporal Inference

Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temporal inference: to compute the likelihood that the execution traces satisfy a given temporal property. This paper presents a general framework for temporal inference, which applies to a rich variety of quantitative models including those that arise in the operational semantics of probabilistic and weighted programs. The key idea underlying our framework is that in a variety of existing approaches, the main construction that enables temporal inference is that of a product between the system of interest and the temporal property. We provide a unifying mathematical definition of product constructions, enabled by the realisation that 1) both systems and temporal properties can be modelled as coalgebras and 2) product constructions are distributive laws in this context. Our categorical framework leads us to our main contribution: a sufficient condition for correctness, which is precisely what enables to use the product construction for temporal inference. We show that our framework can be instantiated to naturally recover a number of disparate approaches from the literature including, e.g., partial expected rewards in Markov reward models, resource-sensitive reachability analysis, and weighted optimization problems. Further, we demonstrate a product of weighted programs and weighted temporal properties as a new instance to show the scalability of our approach.

cs.LO↗

arXiv2024

Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination

Active learning of finite automata has been vigorously pursued for the purposes of analysis and explanation of black-box systems. In this paper, we study an L*-style learning algorithm for weighted automata over the max-plus semiring. The max-plus setting exposes a "consistency" issue in the previously studied semiring-generic extension of L*: we show that it can fail to maintain consistency of tables, and can thus make equivalence queries on obviously wrong hypothesis automata. We present a theoretical fix by a mathematically clean notion of column-closedness. We also present a nontrivial and reasonably broad class of weighted languages over the max-plus semiring in which our algorithm terminates.

cs.FL↗

arXiv2024

Compositional Value Iteration with Pareto Caching

The de-facto standard approach in MDP verification is based on value iteration (VI). We propose compositional VI, a framework for model checking compositional MDPs, that addresses efficiency while maintaining soundness. Concretely, compositional MDPs naturally arise from the combination of individual components, and their structure can be expressed using, e.g., string diagrams. Towards efficiency, we observe that compositional VI repeatedly verifies individual components. We propose a technique called Pareto caching that allows to reuse verification results, even for previously unseen queries. Towards soundness, we present two stopping criteria: one generalizes the optimistic value iteration paradigm and the other uses Pareto caches in conjunction with recent baseline algorithms. Our experimental evaluations shows the promise of the novel algorithm and its variations, and identifies challenges for future work.

cs.LO↗

arXiv2024

Temporal Logic Formalisation of ISO 34502 Critical Scenarios: Modular Construction with the RSS Safety Distance

As the development of autonomous vehicles progresses, efficient safety assurance methods become increasingly necessary. Safety assurance methods such as monitoring and scenario-based testing call for formalisation of driving scenarios. In this paper, we develop a temporal-logic formalisation of an important class of critical scenarios in the ISO standard 34502. We use signal temporal logic (STL) as a logical formalism. Our formalisation has two main features: 1) modular composition of logical formulas for systematic and comprehensive formalisation (following the compositional methodology of ISO 34502); 2) use of the RSS distance for defining danger. We find our formalisation comes with few parameters to tune thanks to the RSS distance. We experimentally evaluated our formalisation; using its results, we discuss the validity of our formalisation and its stability with respect to the choice of some parameter values.

cs.RO↗

arXiv2024

Efficient Matching with Memoization for Regexes with Look-around and Atomic Grouping (Extended Version)

Regular expression (regex) matching is fundamental in many applications, especially in web services. However, matching by backtracking -- preferred by most real-world implementations for its practical performance and backward compatibility -- can suffer from so-called catastrophic backtracking, which makes the number of backtracking super-linear and leads to the well-known ReDoS vulnerability. Inspired by a recent algorithm by Davis et al. that runs in linear time for (non-extended) regexes, we study efficient backtracking matching for regexes with two common extensions, namely look-around and atomic grouping. We present linear-time backtracking matching algorithms for these extended regexes. Their efficiency relies on memoization, much like the one by Davis et al.; we also strive for smaller memoization tables by carefully trimming their range. Our experiments -- we used some real-world regexes with the aforementioned extensions -- confirm the performance advantage of our algorithms.

cs.PL↗

arXiv2024

Pareto Curves for Compositionally Model Checking String Diagrams of MDPs

Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considers string diagrams, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form a Pareto curve on a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach.

cs.LO↗