Search

Abstract: Grabmayer, Endrullis, Hendriks, Klop, and Moss [C. Grabmayer, J. Endrullis, D. Hendriks, J.W. Klop, and L.S. Moss. Automatic sequences and zipspecifications. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, pages 335–344. IEEE Computer Society, 2012] developed a method for defining automatic sequences in terms of ʼzip specificationsʼ and proved that a sequence is automatic [J.-P. Allouche and J. Shallit. Automatic Sequences. Cambridge University Press, 2003] iff it has a zip specification where all zip terms have the same arity. This paper begins by investigating a similar definitional scheme for the higher-dimensional counterpart of automatic sequences, automatic arrays. In the course of establishing the results required for this machinery, we find an isomorphism–closely related to the z-order curve [G.M. Morton. A computer oriented geodetic data base and a new technique in file sequencing. International Business Machines Company, 1966]–between a final coalgebra for arrays and the standard final coalgebra for sequences. This isomorphism preserves automaticity properties: an array is k,l-automatic iff its corresponding sequence is kl-automatic. The former notion of automaticity (k,l-automatic, note the comma) is defined for arrays as in [J.-P. Allouche and J. Shallit. Automatic Sequences. Cambridge University Press, 2003], and the latter notion is the standard notion of automaticity for sequences. It also provides a convenient way to translate between stream zip specifications and array zip specifications. [Copyright &y& Elsevier]

Abstract: The popularity of service-oriented computing has not been accompanied by the necessary formalization of the notions being involved. This paper focuses on the development of a coalgebraic framework to support service-oriented application design. In this paper, the concepts are separated into three hierarchies – interfaces, contracts and services. Interfaces are specified by functors, and services are shown to be coalgebras of such functors, which should satisfy the axioms given in corresponding contracts. Different interfaces, contracts and services are related respectively by the morphisms between them. And the notion of bisimulation for services is derived from service morphisms, which captures the observational equivalence of services. [Copyright &y& Elsevier]

In this paper we show that it is possible to model observable behaviour of coalgebras independently from their internal dynamics, but within the general framework of representing behaviour by a map into a “final” coalgebra.In the first part of the paper we characterise Set-endofunctors F with the property that bisimilarity of elements of F-coalgebras coincides with having the same observable behaviour. We show that such functors have the final coalgebra of a rather simple nature, and preserve some weak pullbacks. We also show that this is the case if and only if F-bisimilarity corresponds to logical equivalence in the finitary fragment of the coalgebraic logic.In the second part of the paper, we present a construction of a “final” coalgebra that captures the observable behaviour of F-coalgebras. We keep the word “final” quoted since the object we are going to construct need not belong to the original category. The construction is carried out for arbitrary Set-endofunctor F, throughout the construction we remain in Set, but the price to pay is the introduction of new morphisms. The paper concludes with a hint to a possible application to modelling weak bisimilarity for coalgebras. [Copyright &y& Elsevier]

A peer-to-peer ( p2p ) system provides the networking substrate for the execution of distributed applications. It is made of peers that interact over an overlay network . Overlay networks are highly dynamic, as peers can join and leave at any time. Traditional process calculi, such as π -calculus, CCS and others, seem inadequate to capture these kinds of networks, their routing mechanisms, and to verify their properties. In order to model network architecture in a more explicit way, in [Ugo Montanari and Matteo Sammartino. Network conscious π -calculus: A concurrent semantics. ENTCS , 286:291–306, 2012; Matteo Sammartino. A Network-Aware Process Calculus for Global Computing and its Categorical Framework. PhD thesis, University of Pisa, 2013. available at http://www.di.unipi.it/~sammarti/publications/thesis.pdf ; Ugo Montanari and Matteo Sammartino. A network-conscious π -calculus and its coalgebraic semantics. Theor. Comput. Sci. , 546:188–224, 2014] we have introduced the Network Conscious π-calculus ( NCPi ), an extension of the π -calculus with names representing network nodes and links. In [Ugo Montanari and Matteo Sammartino. A network–conscious π -calculus and its coalgebraic semantics. Theor. Comput. Sci. , 546:188–224, 2014] (a simpler version of) NCPi has been equipped with a coalgebraic operational models, along the lines of Fiore-Turi presheaf-based approach [Marcelo P. Fiore and Daniele Turi. Semantics of name and value passing. In LICS 2001 , pages 93–104. IEEE Computer Society, 2001], and with an equivalent History Dependent Automaton [Ugo Montanari and Marco Pistore. Structured coalgebras and minimal hd-automata for the π -calculus. Theor. Comput. Sci. , 340(3):539–576, 2005], i.e., an (often) finite-state automaton suitable for verification. In this paper we first give a brief account of these results. Then, our contribution is the sketch of a NCPi representation of the p2p architecture Pastry . In particular, we give models of its overlay network and of a Distributed Hash Table built on top of it, and we give evidence of their correctness by proving convergence of routing mechanisms. [ABSTRACT FROM AUTHOR]

Resumptions appear in many forms as a convenient abstraction, such as in semantics of concurrency and as a programming pattern. In this paper we introduce generalised resumptions in a category-theoretic, coalgebraic context and show their basic properties: they form a monad, they come equipped with a corecursion scheme in the sense of Adámek et al. 's notion of completely iterative monads (cims), and they enjoy a certain universal property, which specialises to the coproduct with a free cim in the category of cims. [ABSTRACT FROM AUTHOR]

Abstract: This paper studies a coalgebraic theory of fuzzy transition systems. Main conclusions include: the functor for deterministic fuzzy transition systems and the functor for nondeterministic fuzzy transition systems preserve weak pullbacks, and the functor has a final coalgebra under some restricted conditions. Moreover, we show how to get a concrete (fuzzy) bisimulation from a coalgebraic bisimulation. [Copyright &y& Elsevier]

Abstract: GSOS is a specification format for well-behaved operations on transition systems. Aceto introduced a restriction of this format, called simple GSOS, which guarantees that the associated transition system is locally finite, i.e. every state has only finitely many different descendent states (i.e. states reachable by a sequence of transitions). The theory of coalgebras provides a framework for the uniform study of systems, including labelled transition systems but also, e.g. weighted transition systems and (non-)deterministic automata. In this context GSOS can be studied at the general level of distributive laws of syntax over behaviour. In the present paper we generalize Acetoʼs result to the setting of coalgebras by restricting abstract GSOS to bipointed specifications. We show that the operational model of a bipointed specification is locally finite, even for specifications with infinitely many operations which have finite dependency. As an example, we derive a concrete format for operations on regular languages and obtain for free that regular expressions have finitely many derivatives modulo the equations of join semilattices. [Copyright &y& Elsevier]

Abstract: Coinductive predicates express persisting “safety” specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a fibration—a categorical abstraction of predicate logic. In this paper we follow the spirit of a seminal work by Worrell and study final sequences in a fibration. Our main contribution is to identify some categorical “size restriction” axioms that guarantee stabilization of final sequences after ω steps. In its course we develop a relevant categorical infrastructure that relates fibrations and locally presentable categories, a combination that does not seem to be studied a lot. The genericity of our fibrational framework can be exploited for: binary relations (i.e. the logic of “binary predicates”) for which a coinductive predicate is bisimilarity; constructive logics (where interests are growing in coinductive predicates); and logics for name-passing processes. [Copyright &y& Elsevier]

Abstract: In a previous paper we introduced internal models for coalgebraic modal logics and showed how they characterise expressivity for bismulation. Here we extend this work by enriching over preordered sets, and in so doing derive a characterisation that subsumes expressivity for both bisimulation and simulation. [Copyright &y& Elsevier]

Abstract: The main result of this paper shows how coalgebraic traces, in suitable Kleisli categories, give rise to traced monoidal structure in those Kleisli categories, with finite coproducts as monoidal structure. At the heart of the matter lie partially additive monads inducing partially additive structure in their Kleisli categories. By applying the standard “Int” construction one obtains compact closed categories for “bidirectional monadic computation”. [ABSTRACT FROM AUTHOR]

Abstract: This paper gives a general coalgebraic account of the notions of possibly infinite trace and possibly infinite execution in state-based, dynamical systems, by extending the generic theory of finite traces and executions developed by Hasuo and coauthors [I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3:1–36, 2007]. The systems we consider are modelled as coalgebras of endofunctors obtained as the composition of a computational type (e.g. nondeterministic or stochastic) with a general transition type. This generalises existing work by Jacobs [B. Jacobs. Trace semantics for coalgebras. In Proc. CMCS 2004, volume 106 of ENTCS, 2004] that only accounts for a nondeterministic computational type. We subsequently introduce path-based temporal (including fixpoint) logics for coalgebras of such endofunctors, whose semantics is based upon the notion of possibly infinite execution. Our approach instantiates to both nondeterministic and stochastic computations, yielding, in particular, path-based fixpoint logics in the style of CTL* for nondeterministic systems, as well as generalisations of the logic PCTL for probabilistic systems. [ABSTRACT FROM AUTHOR]

Abstract: The notion of arrow by Hughes is an axiomatization of the algebraic structure possessed by structured computations in general. We claim that an arrow also serves as a basic component calculus for composing state-based systems as components—in fact, it is a categorified version of arrow that does so. In this paper, following the second author''s previous work with Heunen, Jacobs and Sokolova, we prove that a certain coalgebraic modeling of components—which generalizes Barbosa''s—indeed carries such arrow structure. Our coalgebraic modeling of components is parametrized by an arrow A that specifies computational structure exhibited by components; it turns out that it is this arrow structure of A that is lifted and realizes the (categorified) arrow structure on components. The lifting is described using the first author''s recent characterization of an arrow as an internal strong monad in Prof, the bicategory of small categories and profunctors. [Copyright &y& Elsevier]

Abstract: In this paper we introduce the notion of an observational coalgebra structure and of a complete set of co-operations. We demonstrate in various example the usefulness of these notions, in particular, we show how they give rise to coalgebraic proof and definition principles. [Copyright &y& Elsevier]

Abstract: Following earlier work, a modal logic for T-coalgebras is a functor L on a suitable variety. Syntax and proof system of the logic are given by presentations of the functor. This paper makes two contributions. First, a previous result characterizing those functors that have presentations is generalized from endofunctors on one-sorted varieties to functors between many-sorted varieties. This yields an equational logic for the presheaf semantics of higher-order abstract syntax. As another application, we show how the move to functors between many-sorted varieties allows to modularly combine syntax and proof systems of different logics. Second, we show how to associate to any set-functor T a complete (finitary) logic L consisting of modal operators and Boolean connectives. [Copyright &y& Elsevier]

Abstract: Subsequential transducers generalise both classic deterministic automata and Mealy/Moore type state machines by combining (input) language recognition with transduction. In this paper we show that normalisation and taking differentials of subsequential transducers and their underlying structures can be seen as coalgebraisation. More precisely, we show that the subclass of normalised subsequential structures is a category of coalgebras which is reflective in the category of coaccessible subsequential structures, and which has a final object. This object is then also final for coaccessible structures. The existence and properties of the minimal subsequential transducer realising a partial word function f can be derived from this result. We also show that subsequential structures in which all states are accepting, can be seen as coalgebras by taking differentials. The coalgebraic representation obtained in this way gives rise to an alternative method of deciding transducer equivalence. [Copyright &y& Elsevier]

Abstract: The bisimulation “up-to-…” technique provides an effective way to relieve the amount of work in proving bisimilarity of two processes. This paper develops a fresh and direct approach to generalize this set-theoretic “up-to-...” principle to the setting of coalgebra theory. The notion of consistent function is introduced, as a generalization of Sangiorgi''s sound function. Then, in order to prove that there are only bisimilar pairs in a relation, it is sufficient to find a morphism from it to the “lifting” of its image under some consistent function. One example is given showing that every self-bisimulation in normed BPA is just such a relation. What''s more, we investigate the connection between span-bisimulation and ref-bisimulation. As a result, λ-bisimulation turns out to be covered by our new principle. [Copyright &y& Elsevier]

Abstract: Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of “non-determinism” such as classical non-determinism (with a set of possible choices) vs. probabilistic non-determinism. In this paper we claim that these various forms of “trace semantics” are instances of a single categorical construction, namely coinduction in a Kleisli category. This claim is based on our main technical result that an initial algebra in the category of sets and functions yields a final coalgebra in the Kleisli category, for monads with a suitable order structure. The proof relies on coincidence of limits and colimits, like in the work of Smyth and Plotkin. [Copyright &y& Elsevier]

Abstract: In Rutten [Rutten, J., Algebraic specification and coalgebraic synthesis of Mealy machines, Technical Report SENR0514, Centrum voor Wiskunde en Informatica (CWI) (2005), to appear in Proceedings FACS 2005] the theoretical basis was given for the synthesis of binary Mealy machines from specifications in 2-adic arithmetic. This construction is based on the symbolic computation of the coalgebraic notion of stream function derivative, a generalisation of the Brzozowski derivative of regular expressions. In this paper we complete the construction of Mealy machines from specifications in both 2-adic and modulo-2 arithmetic by describing how we decide equivalence of expressions via reduction to normal forms; we present a Haskell implementation of this Mealy synthesis algorithm; and a theoretical result which characterises the (number of) states in Mealy machines constructed from rational 2-adic specifications. [Copyright &y& Elsevier]

Abstract: This paper gives an overview of recent results concerning the modular derivation of (i) modal specification logics, (ii) notions of simulation together with logical characterisations, and (iii) sound and complete axiomatisations, for systems modelled as coalgebras of functors on Set. Our approach applies directly to an inductively-defined class of coalgebraic types, which subsumes several types of discrete state-based systems, including (probabilistic) transition systems, probabilistic automata and spatial transition systems. [Copyright &y& Elsevier]

Abstract: In this paper, we look at two categorical accounts of computational effects (strong monad as a model of the monadic metalanguage, adjunction as a model of call-by-push-value with stacks), and we adapt them to incorporate global exceptions. In each case, we extend the calculus with a construct, due to Benton and Kennedy, that fuses exception handling with sequencing. This immediately gives us an equational theory, simply by adapting the equations for sequencing. We study the categorical semantics of the two equational theories. In the case of the monadic metalanguage, we see that a monad supporting exceptions is a coalgebra for a certain comonad. We further show, using Beck''s theorem, that, on a category with equalizers, the monad constructor for exceptions gives all such monads. In the case of call-by-push-value (CBPV) with stacks, we generalize the notion of CBPV adjunction so that a stack awaiting a value can deal both with a value being returned, and with an exception being raised. We see how to obtain a model of exceptions from a CBPV adjunction, and vice versa by restricting to those stacks that are homomorphic with respect to exception raising. [Copyright &y& Elsevier]

Abstract: For algebras A whose type is given by an endofunctor, iterativity means that every flat equation morphism in A has a unique solution. In our previous work we proved that every object generates a free iterative algebra, and we provided a coalgebraic construction of those free algebras. Iterativity w.r.t. an endofunctor was generalized by Tarmo Uustalu to iterativity w.r.t. a “base”, i.e., a functor of two variables yielding finitary monads in one variable. In the current paper we introduce iterative algebras in this general setting, and provide again a coalgebraic construction of free iterative algebras. [Copyright &y& Elsevier]

Abstract: Iterative theories introduced by Calvin Elgot formalize potentially infinite computations as solutions of recursive equations. One of the main results of Elgot and his coauthors is a description of a free iterative theory as the theory of all rational trees. Their algebraic proof of this fact is extremely complicated. In our paper we show that by starting with “iterative algebras”, i. e., algebras admitting a unique solution of all systems of flat recursive equations, a free iterative theory is obtained as the theory of free iterative algebras. The (coalgebraic) proof we present is dramatically simpler than the original algebraic one. And our result is, nevertheless, much more general: we describe a free iterative theory on any finitary endofunctor of every locally presentable category . This allows us, e. g., to consider iterative algebras over any equationally specified class of finitary algebras. [Copyright &y& Elsevier]

Abstract: It is the aim of this paper to generalize existing connections between automata and logic to a more general, coalgebraic level. Let be a standard functor that preserves weak pullbacks. We introduce the notion of an F-automaton, a device that operates on pointed F-coalgebras; the criterion under which such an automaton accepts or rejects a pointed coalgebra is formulated in terms of an infinite two-player graph game. We also introduce a language of coalgebraic fixed point logic for F-coalgebras, and we provide a game semantics for this language. Finally we show that any formula p of the language can be transformed into an F-automaton which is equivalent to p in the sense that accepts precisely those pointed F-coalgebras in which p holds. [Copyright &y& Elsevier]

Abstract: Relation lifting [Hermida, C. and B. Jacobs, Structural induction and coinduction in a fibrational setting, Information and Computation 145 (1998), pp. 107–152] extends an endofunctor to a functor , where is a suitable category of relations over . The relation lifting for the functor F can be used to define the notion of bisimulation for coalgebras . The related notion of predicate lifting can be used to define invariants for F–coalgebras. Predicate and relation lifting can be directly defined for a rich class of polynomial functors [Hensel, U. and B. Jacobs, Proof principles for datatypes with iterated recursion, in: E. Moggi and G. Rosolini, editors, Category Theory and Computer Science, LNCS 1290 (1997), pp. 220–241; Hermida, C. and B. Jacobs, Structural induction and coinduction in a fibrational setting, Information and Computation 145 (1998), pp. 107–152; Tews, H., Coalgebras for binary methods: Properties of bisimulations and invariants, Theoretical informatics and applications 35 (2001), pp. 83–111]. In this paper I investigate the case where the functor F is defined as the initial semantics of a (single sorted) parametric algebraic specification. [Copyright &y& Elsevier]

Abstract: This paper connects coalgebra with a long discussion in the foundations of game theory on the modeling of type spaces. We argue that type spaces are coalgebras, that universal type spaces are final coalgebras, and that the modal logics already proposed in the economic theory literature are closely related to those in recent work in coalgebraic modal logic. In the other direction, the categories of interest in this work are usually measurable spaces or compact (Hausdorff) topological spaces. A coalgebraic version of the construction of the universal type space due to Heifetz and Samet [Journal of Economic Theory 82 (2) (1998) 324–341] is generalized for some functors in those categories. Since the concrete categories of interest have not been explored so deeply in the coalgebra literature, we have some new results. We show that every functor on the category of measurable spaces built from constant functors, products, coproducts, and the probability measure space functor has a final coalgebra. Moreover, we construct this final coalgebra from the relevant version of coalgebraic modal logic. Specifically, we consider the set of theories of points in all coalgebras and endow this set with a measurable and coalgebra structure. [Copyright &y& Elsevier]

Abstract: In an attempt to devise a general notion of model for spatial logic, we have been led to consider transition systems with an additional so-called spatial structure on the states, with both the tran- sition and the spatial structures described in coalgebraic terms. In this paper we argue that such transition systems with spatial structure can be seen as a noninterleaving model of concurrency, by providing translations to and from a certain category of Petri nets. [Copyright &y& Elsevier]

Abstract: In this paper we construct a setting in which the question of when a logic supports a classical modal expansion can be made precise. Given a fully selfextensional logic , we find sufficient conditions under which the Vietoris endofunctor on -referential algebras can be defined and we propose to define the modal expansions of as the logic that arises from the -coalgebras. As an example, we also show how the Vietoris endofunctor on referential algebras extends the Vietoris endofunctor on Stone spaces. From another point of view, we examine when a category of ''spaces'', ie sets X equipped with an algebra of subsets of X, allows for the definition of powerspaces (and hence transition systems ). [Copyright &y& Elsevier]

Abstract: With coalgebras usually being defined in terms of an endofunctor T on sets, this paper shows that modal logics for T-coalgebras can be naturally described as functors L on boolean algebras. Building on this idea, we study soundness, completeness and expressiveness of coalgebraic logics from the perspective of duality theory. That is, given a logic for coalgebras of an endofunctor T, we construct an endofunctor L such that L-algebras provide a sound and complete (algebraic) semantics of the logic. We show that if L is dual to T, then soundness and completeness of the algebraic semantics immediately yield the corresponding property of the coalgebraic semantics. We conclude by characterising duality between L and T in terms of the axioms of . This provides a criterion for proving concretely given logics to be sound, complete and expressive. [Copyright &y& Elsevier]