arXiv subjects

Yuichi Komorida

Publications and source records attributed to Yuichi Komorida.

4 recordsLinked to original sources

arXiv2024

Explicit Hopcroft's Trick in Categorical Partition Refinement

Algorithms for partition refinement are actively studied for a variety of systems, often with the optimisation called Hopcroft's trick. However, the low-level description of those algorithms in the literature often obscures the essence of Hopcroft's trick. Our contribution is twofold. Firstly, we present a novel formulation of Hopcroft's trick in terms of general trees with weights. This clean and explicit formulation -- we call it Hopcroft's inequality -- is crucially used in our second contribution, namely a general partition refinement algorithm that is functor-generic (i.e. it works for a variety of systems such as (non-)deterministic automata and Markov chains). Here we build on recent works on coalgebraic partition refinement but depart from them with the use of fibrations. In particular, our fibrational notion of $R$-partitioning exposes a concrete tree structure to which Hopcroft's inequality readily applies. It is notable that our fibrational framework accommodates such algorithmic analysis on the categorical level of abstraction.

cs.FL↗

arXiv2021

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

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 (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting -- a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by König et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.

cs.LO↗

arXiv2021

Injective Objects and Fibered Codensity Liftings

Functor lifting along a fibration is used for several different purposes in computer science. In the theory of coalgebras, it is used to define coinductive predicates, such as simulation preorder and bisimilarity. Codensity lifting is a scheme to obtain a functor lifting along a fibration. It generalizes a few previous lifting schemes including the Kantorovich lifting. In this paper, we seek a property of functor lifting called fiberedness. Hinted by a known result for Kantorovich lifting, we identify a sufficient condition for a codensity lifting to be fibered. We see that this condition applies to many examples that have been studied. As an application, we derive some results on bisimilarity-like notions.

cs.LO↗

arXiv2019

Codensity Games for Bisimilarity

Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, etc.), bisimilarity has been extended in various ways: notably, bisimulation metric between probabilistic systems. An important feature of bisimilarity is its game-theoretic characterization, where Spoiler and Duplicator play against each other; extension of bisimilarity games to quantitative settings has been actively pursued too. In this paper, we present a general framework that uniformly describes game characterizations of bisimilarity-like notions. Our framework is formalized categorically using fibrations and coalgebras. In particular, our characterization of bisimilarity in terms of fibrational predicate transformers allows us to derive codensity bisimilarity games: a general categorical game characterization of bisimilarity. Our framework covers known bisimilarity-like notions (such as bisimulation metric) as well as new ones (including what we call bisimulation topology).

cs.LO↗