188 research outputs found
Coalgebraic Infinite Traces and Kleisli Simulations
No full textKleisli 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 types of systems. A generic categorical theory behind Kleisli simulation has been developed and it guarantees the soundness of those simulations wrt. finite trace semantics. Moreover, those simulations can be aided by forward partial execution (FPE) - a categorical transformation of systems previously introduced by the authors.
In this paper, we give Kleisli simulation a theoretical foundation that assures its soundness also wrt. infinite trace. There, following Jacobs' work, infinite trace semantics is characterized as the "largest homomorphism." It turns out that soundness of forward simulations is rather straightforward; that of backward simulation holds too, although it requires certain additional conditions and its proof is more involved. We also show that FPE can be successfully employed in the infinite trace setting to enhance the applicability of Kleisli simulations as witnesses of trace inclusion. Our framework is parameterized in the monad for branching as well as in the functor for linear-time behaviors; for the former we use the powerset monad (for nondeterminism) as well as the sub-Giry monad (for probability)
Coalgebras and Higher-Order Computation: a GoI Approach
No full textGirard's geometry of interaction (GoI) can be seen---in one practical
aspect of it---as a compositional compilation method from functional
programs to sequential machines. There tokens move around and express
interactions between (parts of) programs. Intrigued by the combination
of abstract structures and concrete dynamics in GoI, our line of work
has aimed at exploiting, in GoI, results from the theory of
coalgebra---a categorical abstraction of state-based transition
systems that has found its use principally in concurrency theory. Such
reinforced connection between higher-order computation and state-based
dynamics is made possible thanks to an elegant categorical
axiomatization of GoI by Abramsky, Haghverdi and Scott, where traced
monoidal categories are identified to be the essential structure
behind. In the talk I shall lay out these basic ideas, together with
some of our results on: GoI semantics for a quantum programming
language; and our ``memoryful'' extension of GoI with algebraic
effects.
The talk is based on my joint work with my colleague Naohiko Hoshino (RIMS, Kyoto Univer- sity) and my (former) students Koko Muroya (University of Birmingham) and Toshiki Kataoka
(University of Tokyo), to whom I owe special thanks
Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial)
No full textCoalgebra is a categorical modeling of state-based dynamics. Final coalgebras - as categorical greatest fixed points - play a central role in the theory; somewhat analogously, most coalgebraic proof techniques have been devoted to greatest fixed-point properties such as safety and bisimilarity. In this tutorial, I introduce our recent coalgebraic framework that accommodates those fixed-point specifications which are not necessarily the greatest. It does so specifically by characterizing the accepted languages of Büchi and parity automata in categorical terms. We present two characterizations of accepted languages. The proof for their coincidence offers a unique categorical perspective of the correspondence between (logical) fixed-point specifications and the (combinatorial) parity acceptance condition
Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective
No full textNotions of simulation, among other uses, provide a computationally tractable
and sound (but not necessarily complete) proof method for language inclusion.
They have been comprehensively studied by Lynch and Vaandrager for
nondeterministic and timed systems; for B\"{u}chi automata the notion of fair
simulation has been introduced by Henzinger, Kupferman and Rajamani. We
contribute to a generalization of fair simulation in two different directions:
one for nondeterministic tree automata previously studied by Bomhard; and the
other for probabilistic word automata with finite state spaces, both under the
B\"{u}chi acceptance condition. The former nondeterministic definition is
formulated in terms of systems of fixed-point equations, hence is readily
translated to parity games and is then amenable to Jurdzi\'{n}ski's algorithm;
the latter probabilistic definition bears a strong ranking-function flavor.
These two different-looking definitions are derived from one source, namely our
coalgebraic modeling of B\"{u}chi automata. Based on these coalgebraic
observations, we also prove their soundness: a simulation indeed witnesses
language inclusion
Parity automata for quantitative linear time logics
No full textWe initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of Büchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naïve algorithm for computing extents, under additional assumptions on the domain of truth values
Lattice-theoretic progress measures and coalgebraic model checking
No full textIn the context of formal verification in general and model checking in particular, parity games serve as a mighty vehicle: many problems are encoded as parity games, which are then solved by the seminal algorithm by Jurdzinski. In this paper we identify the essence of this workflow to be the notion of progress measure, and formalize it in general, possibly infinitary, lattice-theoretic terms. Our view on progress measures is that they are to nested/alternating fixed points what invariants are to safety/greatest fixed points, and what ranking functions are to liveness/least fixed points. That is, progress measures are combination of the latter two notions (invariant and ranking function) that have been extensively studied in the context of (program) verification. We then apply our theory of progress measures to a general model-checking framework, where systems are categorically presented as coalgebras. The framework's theoretical robustness is witnessed by a smooth transfer from the branching-time setting to the linear-time one. Although the framework can be used to derive some decision procedures for finite settings, we also expect the proposed framework to form a basis for sound proof methods for some undecidable/infinitary problems
Decision Tree Learning in CEGIS-Based Termination Analysis
No full textThis is a docker image containing a termination analyzer, MuVal [1].
You can load and run the image by the following commands.
sudo docker load -i cav21ae.tar
sudo docker run -it coar:cav21ae_dt /bin/bash --login
See /home/muval/coar/cav21ae_dt/README.md or our github repository for details.
[1] Satoshi Kura, Hiroshi Unno, and Ichiro Hasuo. Decision Tree Learning in CEGIS-Based Termination Analysis. CAV 2021
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
No full textThe coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata
Coalgebraic Trace Semantics for Buechi and Parity Automata
No full textDespite 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 notion in the
theory of automata for infinite words or trees. In this paper we present a clean answer to the question that builds on the "maximality" characterization of infinite traces (by Jacobs and Cirstea): the accepted language of a Buechi automaton is characterized by two commuting diagrams, one for a least homomorphism and the other for a greatest, much like in a system of (least and greatest) fixed-point equations. This characterization works uniformly for the nondeterministic branching and the probabilistic one; and for words and trees alike. We present our results in terms of the parity acceptance condition that generalizes Buechi's
Coalgebraic CTL: fixpoint characterization and polynomial-time model checking
No full textWe introduce a path-based coalgebraic temporal logic, CoalgebraicCTL (CCTL), as a categorical abstraction of standard ComputationTree Logic (CTL). Our logic can be used to formalize propertiesof systems modeled as coalgebras with branching. We present the syntaxand path-based semantics of CCTL, and show how to encode this logicinto a coalgebraic fixpoint logic with a step-wise semantics. Our mainresult shows that this encoding is semantics-preserving. We also presenta polynomial-time model-checking algorithm for CCTL, inspired by thestandard model-checking algorithm for CTL but described in categoricalterms. A key contribution of our paper is to identify the categoricalessence of the standard encoding of CTL into the modal mu-calculus.This categorical perspective also explains the absence of a similar encodingof PCTL (Probabilistic CTL) into the probabilistic mu-calculus
- …
