activity
20072025
most citedGeneric Trace Semantics via Coinduction

88 citations · 339 across the 67 of their papers we have counts for

collaborators
Showing 2021Show all

8 papers · 1 filter

cs.GT2021★ 6 cited

A Compositional Approach to Parity Games

Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada +1

In this paper, we introduce open parity games, which is a compositional approach to parity games. This is achieved by adding open ends to the usual notion of parity games. We intro…

cs.SE2021★ 10 cited

Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty

Tsutomu Kobayashi, Rick Salay, Ichiro Hasuo +3

Formal reasoning on the safety of controller systems interacting with plants is complex because developers need to specify behavior while taking into account perceptual uncertainty…

cs.SE2021★ 1 cited

Architecture-Guided Test Resource Allocation Via Logic

Clovis Eberhart, Akihisa Yamada, Stefan Klikovits +4

We introduce a new logic named Quantitative Confidence Logic (QCL) that quantifies the level of confidence one has in the conclusion of a proof. By translating a fault tree represe…

cs.LO2021★ 1 cited

Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation

Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke +2

A modal logic that is strong enough to fully characterize the behavior of a system is called expressive. Recently, with the growing diversity of systems to be reasoned about (proba…

cs.LO2021★ 2 cited

Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

Mayuko Kori, Ichiro Hasuo, Shin-ya Katsumata

The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, w…

cs.LO2021

Decision Tree Learning in CEGIS-Based Termination Analysis

Satoshi Kura, Hiroshi Unno, Ichiro Hasuo

We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample G…