Search

Simulations are a very natural way of relating concurrent systems, which are mathematically modeled by Kripke structures. The range of available notions of simulations makes it very natural to adopt a categorical viewpoint in which Kripke structures become the objects of several categories while the morphisms are obtained from the corresponding notion of simulation. Here we define in detail several of those categories, collect them together in various institutions, and study their most interesting properties. [ABSTRACT FROM AUTHOR]

This paper provides a general account of the notion of recursive program schemes, their uninterpreted and interpreted solutions, and related concepts. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with "enough final coalgebras" we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered, or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study recursion, e. g., substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes at all. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme. In this short version of our paper we can only sketch some proofs. [ABSTRACT FROM AUTHOR]

In this paper we present FLRS, a sound and complete equational logic for proving the equivalence of recursive program schemes. We use extended versions of the Solution Theorems from [1] and [2] to provide coalgebraic semantics to recursive program schemes. We end the paper with a proof that FLRS is complete with respect to the coalgebraic semantics. [ABSTRACT FROM AUTHOR]

This paper studies finitary modal logics as specification languages for Set-coalgebras (coalgebras on the category of sets) using Stone duality. It is well-known that Set-coalgebras are not semantically adequate for finitary modal logics in the sense that bisimilarity does not in general coincide with logical equivalence. Stone-coalgebras (coalgebras over the category of Stone spaces), on the other hand, do provide an adequate semantics for finitary modal logics. This leads us to study the relationship of finitary modal logics and Set-coalgebras by uncovering the relationship between Set-coalgebras and Stone-coalgebras. This builds on a long tradition in modal logic, where one studies canonical extensions of modal algebras and ultrafilter extensions of Kripke frames to account for finitary logics. Our main contributions are the generalisations of two classical theorems in modal logic to coalgebras, namely the Jónsson-Tarski theorem giving a set-theoretic representation for each modal algebra and the bisimulation-somewhere-else theorem stating that two states of a coalgebra have the same (finitary modal) theory iff they are bisimilar (or behaviourally equivalent) in the ultrafilter extension of the coalgebra. [ABSTRACT FROM AUTHOR]

Every endofunctor B on the category can be lifted to a fibred functor on the category (fibred over ) of equivalence relations and relation-preserving functions. In this paper, the least (fibre-wise) of such liftings, L(B), is characterized for essentially any B. The lifting has all the useful properties of the relation lifting due to Jacobs, without the usual assumption of weak pullback preservation; if B preserves weak pullbacks, the two liftings coincide. Equivalence relations can be viewed as Boolean algebras of subsets (predicates, tests). This correspondence relates L(B) to the least test suite lifting T(B), which is defined in the spirit of predicate lifting as used in coalgebraic modal logic. Properties of T(B) translate to a general expressivity result for a modal logic for B-coalgebras. In the resulting logic, modal operators of any arity can appear. [ABSTRACT FROM AUTHOR]

Recently, various process calculi have been introduced which are suited for the modelling of mobile computation and in particular the mobility of program code; a prominent example is the ambient calculus. Due to the complexity of the involved spatial reduction, there is — in contrast to the situation in standard process algebra — up to now no satisfying coalgebraic representation of a mobile process calculus. Here, we discuss work towards a unifying coalgebraic framework for the denotational semantics of mobile systems. The connection between the ambient calculus and a coalgebraic approach which uses an extension of labelled transition systems in the representation of the reduction relation is analyzed in more detail. The formal representation of this framework is cast in the algebraic-coalgebraic specification language CoCasl. [ABSTRACT FROM AUTHOR]

We show that, for functors with suitable mild restrictions, the initial algebra in the category of sets and functions gives rise to the final coalgebra in the (Kleisli) category of sets and relations. The finality principle thus obtained leads to the finite trace semantics of non-deterministic systems, which extends the trace semantics for coalgebras previously introduced by the second author. We demonstrate the use of our technical result by giving the first coalgebraic account on context-free grammars, where we obtain generated context-free languages via the finite trace semantics. Additionally, the constructions of both finite and possibly infinite parse trees are shown to be monads. Hence our extension of the application domain of coalgebras identifies several new mathematical constructions and structures. [ABSTRACT FROM AUTHOR]

For any set-endofunctor there exists a largest sub-cartesian transformation μ to the filter functor . Thus we can associate with every T-coalgebra A a certain filter-coalgebra . Precisely, when T (weakly) preserves preimages, μ is natural, and when T (weakly) preserves intersections, μ factors through the covariant powerset functor , thus providing for every T-coalgebra A a Kripke structure . We characterize preservation of preimages, preservation of intersections, and preservation of both preimages and intersections via the existence of natural, sub-cartesian or cartesian transformations from T to either or . Moreover, we define for arbitrary T-coalgebras a next-time operator with associated modal operators and and relate their properties to weak limit preservation properties of T. In particular, for any T-coalgebra there is a transition system with if and only if T preserves intersections. [ABSTRACT FROM AUTHOR]

In the specific situation of formal reasoning concerned with "regular expression equivalence" we address instances of more general questions such as: how can coinductive argumentation be formalised logically and be applied effectively, as well as how is it linked to traditional forms of proof. For statements expressing that two regular expressions are language equivalent, we demonstrate that proofs by coinduction can be formulated in a proof system based on equational logic, where effective proof-search is possible. And we describe a proof-theoretic method for translating derivations in this proof system into a "traditional" axiom system: namely, into a "reverse form" of the axiomatisation of "regular expression equivalence" due to Salomaa. Hereby we obtain a coinductive completeness proof for the traditional proof system. [ABSTRACT FROM AUTHOR]

The proof system has been used to implement an algebraic framework for verifying the correctness of hardware with input and output. Implementations and specifications are modelled as iterated maps, with input and output modelled using streams. The correctness model supports three types of abstraction: temporal abstraction (with immersions), data abstraction, and stream abstraction. This work has been used to formally verify the 6 microprocessor. This paper discusses this processor's input and output behaviour and shows how this has been modelled and verified in . The verification is believed to be the first complete formal verification of a commercial off-the-shelf (COTS) processor. The definition of correctness given here is new - it is suited to verifying block data transfer instructions, these load and store sets of registers. [ABSTRACT FROM AUTHOR]

We propose a coalgebraic model of the Fusion calculus based on HD-automata. The main advantage of the approach is that the partition refinement algorithm designed for HD-automata is easily adapted to handle Fusion calculus processes. Hence, the transition systems of Fusion calculus processes can be minimised according to the notion of observational semantics of the calculus. As a beneficial side effect, this also provides a bisimulation checker for Fusion calculus. [ABSTRACT FROM AUTHOR]

Simple systems cannot decomposed further. Algebraically, simple systems have only isomorphisms as epis. We characterize simple stochastic relations through different forms of bisimulations for the case that the underlying spaces are Polish, and analytic, respectively. This requires a closer investigation of bisimulations, congruences and their mutual relationship. We provide a complete characterization of simple stochastic relations for analytic spaces. [ABSTRACT FROM AUTHOR]

There are several approaches to the problem of giving a categorical semantics to Martin-Löf type theory with dependent sums and products and extensional equality types. The most established one relies on the notion of a type-category (or category with attributes) with Σ and Π types. We extend such a semantics by introducing coinductive types both on the syntactic level and in a type-category. Soundness of the semantics is preserved. As an example of such a category, we prove that the type-category built over a locally cartesian closed category admits coinductive types whenever has final coalgebras for all polynomial functors. [ABSTRACT FROM AUTHOR]

The conceptual separation between computation and coordination in distributed computing systems motivates the use of peculiar entities commonly called connectors, whose task is managing the interaction among distributed components. Different kinds of connectors exist in the literature, at different levels of abstraction. We focus on a basic algebra of connectors which is expressive enough to model, e.g., all the architectural connectors of CommUnity. We first define the operational, observational and denotational semantics of connectors, then we show that the observational and denotational semantics coincide and finally we give a complete normal-form axiomatization. [ABSTRACT FROM AUTHOR]

We present ACPc, a process algebra with conditional expressions in which the conditions are taken from a Boolean algebra, and extensions of this process algebra with mechanisms for condition evaluation. We confine ourselves to finitely branching processes. This restriction makes it possible to presentc in a concise and intuitively clear way, and to bring the notion of splitting bisimulation equivalence and the issue of condition evaluation in process algebras with conditional expressions to the forefront. [ABSTRACT FROM AUTHOR]

The intersection of algebra and coalgebra, i.e., the collection of all categories that are varieties as well as covarieties, is proved to consist of precisely the presheaf categories. [ABSTRACT FROM AUTHOR]

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop's Basic Process Algebra with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based. [ABSTRACT FROM AUTHOR]

We consider open terms and parametric rules in the context of the systematic derivation of labelled transitions from reduction systems. [ABSTRACT FROM AUTHOR]

We study structures which have arisen in recent work by the present author and Bob Coecke on a categorical axiomatics for Quantum Mechanics; in particular, the notion of strongly compact closed category. We explain how these structures support a notion of scalar which allows quantitative aspects of physical theory to be expressed, and how the notion of strong compact closure emerges as a significant refinement of the more classical notion of compact closed category. We then proceed to an extended discussion of free constructions for a sequence of progressively more complex kinds of structured category, culminating in the strongly compact closed case. The simple geometric and combinatorial ideas underlying these constructions are emphasized. We also discuss variations where a prescribed monoid of scalars can be ‘glued in' to the free construction. [ABSTRACT FROM AUTHOR]