Author name cluster

Ichiro Hasuo

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

FM Conference 2026 Conference Paper

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

Radu-Florin Tulcan
Rose Bohrer
Yoàv Montacute
Kevin Zhou
Yusuke Kawamoto 0001
Ichiro Hasuo

Abstract 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.

DOI

FM Conference 2026 Conference Paper

STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP

Martin Jouve-Genty
Han Su
Sota Sato
Jie An
Zhenya Zhang
Ichiro Hasuo

Abstract 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.

DOI

TCS Journal 2025 Journal Article

Strategy templates for almost-sure and positive winning of stochastic parity games towards permissive and resilient control

Kittiphon Phalakarn
Sasinee Pruekprasert
Ichiro Hasuo

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.

Details DOI

AAAI Conference 2020 Conference Paper

Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces

Takamasa Okudono
Masaki Waga
Taro Sekiyama
Ichiro Hasuo

We present a method to extract a weighted ﬁnite automaton (WFA) from a recurrent neural network (RNN). Our method is based on the WFA learning algorithm by Balle and Mohri, which is in turn an extension of Angluin’s classic L∗ algorithm. Our technical novelty is in the use of regression methods for the so-called equivalence queries, thus exploiting the internal state space of an RNN to prioritize counterexample candidates. This way we achieve a quantitative/weighted extension of the recent work by Weiss, Goldberg and Yahav that extracts DFAs. We experimentally evaluate the accuracy, expressivity and efﬁciency of the extracted WFAs.

PDF Details

I&C Journal 2017 Journal Article

Quantitative simulations by matrices

Natsuki Urabe
Ichiro Hasuo

We introduce notions of simulation between semiring-weighted automata as models of quantitative systems. Our simulations are instances of the categorical/coalgebraic notions previously studied by Hasuo—hence soundness against language inclusion comes for free—but are concretely presented as matrices that are subject to linear inequality constraints. Pervasiveness of these formalisms allows us to exploit existing algorithms in: searching for a simulation, and hence verifying quantitative correctness that is formulated as language inclusion. Transformations of automata that aid search for simulations are introduced, too. This verification workflow is implemented for the plus-times and max-plus semirings. Furthermore, an extension to weighted tree automata is presented and implemented.

Details DOI

TCS Journal 2015 Journal Article

Generic weakest precondition semantics from monads enriched with order

Ichiro Hasuo

We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs' recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as “may” vs. “must”) are captured by Eilenberg–Moore algebras; (2) nested alternating branching—like in games and in probabilistic systems with nondeterministic environments—is modularly modeled by a monad on the Eilenberg–Moore category of another.

Details DOI

TCS Journal 2010 Journal Article

Probabilistic anonymity via coalgebraic simulations

Ichiro Hasuo
Yoshinobu Kawabe
Hideki Sakurada

There is a growing concern about anonymity and privacy on the Internet, resulting in lots of work on formalization and verification of anonymity. In particular, the importance of probabilistic aspects of anonymity has recently been highlighted by many authors. Several different notions of “probabilistic anonymity” have been studied so far, but proof methods for such probabilistic notions have not yet been elaborated. In this paper we introduce a simulation-based proof method for one notion of probabilistic anonymity introduced by Bhargava and Palamidessi, called strong probabilistic anonymity. The method is a probabilistic adaptation of the one by Kawabe, Sakurada et al. for non-deterministic anonymity; anonymity of a protocol is proved by finding a forward/backward simulation between certain automata. For the jump from non-determinism to probability we exploit a generic, coalgebraic theory of traces and simulations developed by Hasuo, Jacobs and Sokolova. In particular, an appropriate notion of probabilistic simulation is obtained as an instantiation of the generic definition, for which soundness theorem comes for free. Additionally, we show how we can use a similar idea to verify a weaker notion of probabilistic anonymity called probable innocence.

Details DOI