Search

The aim of the paper is to show the existence of some ingredients for an umbral calculus on some Ore extensions, in a manner analogous to Rota's classical umbral calculus which deals with a univariate polynomial ring on a field of characteristic zero. For that, we introduce the notion of a quasi-derivation in order to specify Ore extensions on which building up this umbral calculus is possible. This allows in particular to define an action of the Ore extension on tensor products of modules. We develop also a Pincherle calculus for operators and we define a coalgebra structure on the Ore extension. [ABSTRACT FROM AUTHOR]

In recent work, Hess and Shipley [18] defined a theory of topological coHochschild homology (coTHH) for coalgebras. In this paper we develop computational tools to study this new theory. In particular, we prove a Hochschild–Kostant–Rosenberg type theorem in the cofree case for differential graded coalgebras. We also develop a coBökstedt spectral sequence to compute the homology of coTHH for coalgebra spectra. We use a coalgebra structure on this spectral sequence to produce several computations. [ABSTRACT FROM AUTHOR]

Abstract: A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analog of Kleene’s theorem and Kleene algebra, were recently proposed by a subset of the authors of this paper. Examples of the systems covered include infinite streams, deterministic automata, Mealy machines and labeled transition systems. In this paper, we present a novel algorithm to decide whether two expressions are bisimilar or not. The procedure is implemented in the automatic theorem prover CIRC, by reducing coinduction to an entailment relation between an algebraic specification and an appropriate set of equations. We illustrate the generality of the tool with three examples: infinite streams of real numbers, Mealy machines and labeled transition systems. [Copyright &y& Elsevier]

Abstract: In an earlier paper we presented a pseudometric on the states of a probabilistic transition system, yielding a quantitative notion of behavioural equivalence. The behavioural pseudometric was defined via the terminal coalgebra of a functor based on a metric on Borel probability measures. In the present paper we give a polynomial-time algorithm, based on linear programming, to calculate the distances between states up to a prescribed degree of accuracy. [Copyright &y& Elsevier]

We study Gentzen-style proof theory of the finitary version of the coalgebraic logic introduced by L. Moss. The logic captures the behaviour of coalgebras for a large class of set functors. The syntax of the logic, defined uniformly with respect to a finitary coalgebraic type functor T , uses a single modal operator ∇ T of arity given by the functor T itself, and its semantics is defined in terms of a relation lifting functor T ¯ . An axiomatization of the logic, consisting of modal distributive laws, has been given together with an algebraic completeness proof in work of C. Kupke, A. Kurz and Y. Venema. In this paper, following our previous work on structural proof theory of the logic in the special case of the finitary powerset functor, we present cut-free, one- and two-sided sequent calculi for the finitary version of Moss' coalgebraic logic for a general finitary functor T in a uniform way. For the two-sided calculi to be cut-free we use a language extended with the boolean dual of the nabla modality. [ABSTRACT FROM AUTHOR]

Abstract: The study of the behaviour of non-deterministic automata has traditionally focused on the languages which can be associated to the different states. Under this interpretation, the different branches that can be taken at every step are ignored. However, we can also take into account the different decisions which can be made at every state, that is, the branches that can be taken, and these decisions might change the possible future behaviour. In this case, the behaviour of the automata can be described with the help of the concept of bisimilarity. This is the kind of description that is usually obtained when the automata are regarded as labelled transition systems or coalgebras. Contrarily to what happens with deterministic automata, it is not possible to describe the behaviour up to bisimilarity of states of a non-deterministic automaton by considering just the languages associated to them. In this paper we present a description of a final object for the category of non-deterministic automata, regarded as labelled transition systems, with the help of some structures defined in terms of languages. As a consequence, we obtain a characterisation of bisimilarity of states of automata in terms of languages and a method to minimise non-deterministic automata with respect to bisimilarity of states. This confirms that languages can be considered as the natural objects to describe the behaviour of automata. [Copyright &y& Elsevier]

Abstract: The contribution of this paper is twofold: first, it defines a unified framework for modelling abstract components, as well as a formalization of integration rules to combine their behaviour. This is based on a coalgebraic definition of components, which is a categorical representation allowing the unification of a large family of formalisms for specifying state-based systems. Second, it studies compositional conformance testing i.e. checking whether an implementation made of correct interacting components combined with integration operators conforms to its specification. [Copyright &y& Elsevier]

Abstract: In this paper, we define a probabilistic version of filtration and use it to provide a finite approximation of Markov processes. In order to measure the approximation, we employ probability logic to construct the final Markov process and define a metric on the set of Markov processes through this logic. Moreover, we show that the set endowed with this metric is a Polish space. Finally we point to some questions connecting approximation to uniformity and approximate bisimilarity as topics for future research. [Copyright &y& Elsevier]

In this paper we give an account of the rise and development of coalgebraic thinking in mathematics and computer science as an illustration of the way mathematical frameworks may be transformed. Originating in a foundational dispute as to the correct way to characterise sets, logicians and computer scientists came to see maximizing and minimizing extremal axiomatisations as a dual pair, each necessary to represent entities of interest. In particular, many important infinitely large entities can be characterised in terms of such axiomatisations. We consider reasons for the delay in arriving at the coalgebraic framework, despite many unrecognised manifestations occurring years earlier, and discuss an apparent asymmetry in the relationship between algebra and coalgebra. [Copyright &y& Elsevier]

Abstract: This paper gives a general coalgebraic account of temporal logics whose semantics involves a notion of computation path. Examples of such logics include the logic CTL* for transition systems and the logic PCTL for probabilistic transition systems. Our path-based temporal logics are interpreted over coalgebras of endofunctors obtained as the composition of a computation type (e.g. non-deterministic or stochastic) with a general transition type. The semantics of such logics relies on the existence of execution maps similar to the trace maps introduced by Jacobs and co-authors as part of the coalgebraic theory of finite traces (Hasuo et al., 2007 ). We consider finite execution maps derived from the theory of finite traces, and a new notion of maximal execution map that accounts for maximal, possibly infinite executions. The latter is needed to recover the logics CTL* and PCTL as specific path-based logics. [Copyright &y& Elsevier]

Abstract: Coalgebras can be seen as a natural abstraction of Kripke frames. In the same sense, coalgebraic logics are generalised modal logics. In this paper, we give an overview of the basic tools, techniques and results that connect coalgebras and modal logic. We argue that coalgebras unify the semantics of a large range of different modal logics (such as probabilistic, graded, relational, conditional) and discuss unifying approaches to reasoning at this level of generality. We review languages defined in terms of the so-called cover modality, languages induced by predicate liftings as well as their common categorical abstraction, and present (abstract) results on completeness, expressiveness and complexity in these settings, both for basic languages as well as a number of extensions, such as hybrid languages and fixpoints. [Copyright &y& Elsevier]

Abstract: Bialgebras and distributive laws are an abstract, categorical framework to study various flavors of structural operational semantics. This paper aims to introduce the reader to the basics of bialgebras for operational semantics, and to sketch the state of the art in this research area. [Copyright &y& Elsevier]

Abstract: The Myhill–Nerode Theorem states that the equivalence relation given by a language has finite index if and only if is accepted by a finite automaton. In this paper we give several generalizations of the theorem which are algebraic in nature. In our versions, a finiteness condition involving the action of a semigroup on a certain function plays the role of the finiteness of the index of , while various algebraic structures including algebras, coalgebras, and bialgebras play the role of the finite automaton which accepts the language. We develop additional theory concerning the algebraic objects which so arise, and study the minimal ones. [ABSTRACT FROM AUTHOR]

Abstract: There is a growing concern about anonymity and privacy on the Internet, resulting in lots of work on formalization and verification of anonymity. In particular, the importance of probabilistic aspects of anonymity has recently been highlighted by many authors. Several different notions of “probabilistic anonymity” have been studied so far, but proof methods for such probabilistic notions have not yet been elaborated. In this paper we introduce a simulation-based proof method for one notion of probabilistic anonymity introduced by Bhargava and Palamidessi, called strong probabilistic anonymity. The method is a probabilistic adaptation of the one by Kawabe, Sakurada et al. for non-deterministic anonymity; anonymity of a protocol is proved by finding a forward/backward simulation between certain automata. For the jump from non-determinism to probability we exploit a generic, coalgebraic theory of traces and simulations developed by Hasuo, Jacobs and Sokolova. In particular, an appropriate notion of probabilistic simulation is obtained as an instantiation of the generic definition, for which soundness theorem comes for free. Additionally, we show how we can use a similar idea to verify a weaker notion of probabilistic anonymity called probable innocence. [Copyright &y& Elsevier]

Abstract: In this paper we construct an adjoint pair of functors between the category of sheaves on a smooth manifold M and the category of coalgebras over the ring of smooth functions with compact support on M. We show that the sheaf coalgebra associated to a sheaf E on M determines the sheaf E uniquely up to an isomorphism, and that the adjoint functors restrict to an equivalence between sheaves on M and sheaf coalgebras over . [Copyright &y& Elsevier]

Abstract: In this paper the familiar construction of the category of coalgebras for a cartesian comonad is extended to the setting of “algebraic set theory”. In particular, it is shown that, under suitable assumptions, several kinds of categories of classes are stable under the formation of coalgebras for a cartesian comonad, internal presheaves and comma categories. [Copyright &y& Elsevier]

Abstract: This paper provides a general account of the notion of recursive program schemes, studying both uninterpreted and interpreted solutions. 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 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. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme. [Copyright &y& Elsevier]

Abstract: A partial component is a process which fails or dies at some stage, thus exhibiting a finite, more ephemeral behaviour than expected. Partiality—which is the rule rather than exception in formal modelling—can be treated mathematically via totalization techniques. In the case of partial functions, totalization involves error values and exceptions. In the context of a coalgebraic approach to component semantics, this paper argues that the behavioural counterpart to such functional techniques should extend behaviour with try-again cycles preventing from component collapse, thus extending totalization or transposition from the algebraic to the coalgebraic context. We show that a refinement relationship holds between original and totalized components which is reasoned about in a coalgebraic approach to component refinement expressed in the pointfree binary relation calculus. As part of the pragmatic aims of this research, we also address the factorization of every such totalized coalgebra into two coalgebraic components—the original one and an added front-end—which cooperate in a client-server style. [Copyright &y& Elsevier]

Abstract: This paper characterises refinement of state-based software components modelled as pointed coalgebras for some Set endofunctors. The proposed characterisation is parametric on a specification of the underlying behaviour model introduced as a strong monad. This provides a basis to reason about (and transform) state-based software designs. In particular, it is shown how refinement can be applied to the development of the inequational subset of a calculus of generic software components. [Copyright &y& Elsevier]

Abstract: This paper presents an application of coinductive stream calculus to signal flow graphs. In comparison to existing approaches, which are usually based on Z-transforms (a discrete version of Laplace transforms) and transfer functions, the model presented in these notes is very elementary. The formal treatment of flow graphs is interesting because it deals with two fundamental phenomena in the theory of computation: memory (in the form of register or delay elements) and infinite behaviour (in the form of feedback). [Copyright &y& Elsevier]

Coalgebras of polynomial functors constructed from sets of observable elements have been found useful in modelling various kinds of data types and state-transition systems. This paper continues the study of equational logic and model theory for polynomial coalgebras begun in Goldblatt (in: Advances in Modal Logic, vol. 4, 2001, to appear), where it was shown that Boolean combinations of equations between terms of observable type form a natural language of observable formulas for specifying properties of polynomial coalgebras, and for giving a Hennessy–Milner style logical characterisation of observational indistinguishability (bisimilarity) of states.Here we give a structural characterisation of classes of coalgebras definable by observable formulas. This is an analogue for polynomial coalgebras of Birkhoff''s celebrated characterisation of equationally definable classes of abstract algebras as being those closed under homomorphic images, subalgebras, and direct products. The coalgebraic characterisation involves new notions of observational ultraproduct and ultrapower of coalgebras, obtained from the classical construction of ultraproducts by deleting states that assign “nonstandard” values to terms of observable type. A class of polynomial coalgebras is shown to be the class of all models of a set of observable formulas if, and only if, it is closed under images of bisimulation relations, disjoint unions and observational ultrapowers.Observational ultraproducts are also used to discuss compactness—which holds only under limited conditions; to characterise finitely, axiomatisable classes of polynomial coalgebras; and to show that there are axiomatisable classes that are not finitely axiomatisable. [Copyright &y& Elsevier]

Infinite trees form a free completely iterative theory over any given signature—this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H( _ )+X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees.This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H⊗_+I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors. [Copyright &y& Elsevier]

This paper describes the basic structures in the denotational and axiomatic semantics of sequential Java, both from a monadic and a coalgebraic perspective. This semantics is an abstraction of the one used for the verification of (sequential) Java programs using proof tools in the LOOP project at the University of Nijmegen. It is shown how the monadic perspective gives rise to the relevant computational structure in Java (composition, extension and repetition), and how the coalgebraic perspective offers an associated program logic (with invariants, bisimulations, and Hoare logics) for reasoning about the computational structure provided by the monad. [Copyright &y& Elsevier]