15 citations · 34 across the 10 of their papers we have counts for
10 papers
Exemplifying parametric timed specifications over signals with bounded behavior
Étienne André, Masaki Waga, Natsuki Urabe +1
Specifying properties can be challenging work. In this paper, we propose an automated approach to exemplify properties given in the form of automata extended with timing constraint…
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata +2
We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious…
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 previo…
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Satoshi Kura, Natsuki Urabe, Ichiro Hasuo
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes…
Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs
Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe +1
Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account on various marti…
Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors
Natsuki Urabe, Ichiro Hasuo
Categorical studies of recursive data structures and their associated reasoning principles have mostly focused on two extremes: initial algebras and induction, and final coalgebras…
Categorical Liveness Checking by Corecursive Algebras
Natsuki Urabe, Masaki Hara, Ichiro Hasuo
Final coalgebras as "categorical greatest fixed points" play a central role in the theory of coalgebras. Somewhat analogously, most proof methods studied therein have focused on gr…
Coalgebraic Trace Semantics for Buechi and Parity Automata
Natsuki Urabe, Shunsuke Shimizu, Ichiro Hasuo
Despite its success in producing numerous general results on state-based dynamics, the theory of coalgebra has struggled to accommodate the Buechi acceptance condition---a basic no…
Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective
Natsuki Urabe, Ichiro Hasuo
Notions of simulation, among other uses, provide a computationally tractable and sound (but not necessarily complete) proof method for language inclusion. They have been comprehens…
Coalgebraic Infinite Traces and Kleisli Simulations
Natsuki Urabe, Ichiro Hasuo
Kleisli simulation is a categorical notion introduced by Hasuo to verify finite trace inclusion. They allow us to give definitions of forward and backward simulation for various ty…