Search

Distributive laws of a monad T over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of context-free languages.

Traditionally, traces are the sequences of labels associated with paths in transition systems X→P(A×X). Here we describe traces more generally, for coalgebras of the form X→P(F(X)), where F is a polynomial functor. The main result states that F's final coalgebra Z→≅F(Z) gives rise to a weakly final coalgebra with state space P(Z), in a suitable category of coalgebras. Weak finality means that there is a coalgebra map X→P(Z), but there is no uniqueness. We show that there is a canonical choice among these maps X→P(Z), namely the largest one, describing the traces in a suitably abstract formulation. A crucial technical ingredient in our construction is a general distributive law FP⇒PF, obtained via relation lifting.

This paper shows that the approach of [P. Aczel, J. Adámek, S. Milius, and J. Velebil, Infinite trees and completely iterative theories: a coalgebraic view, Theor. Comp. Sci., 300 (1-3):1–45, 2003; L.S. Moss, Parametric corecursion, Theor. Comp. Sci., 260(1-2):139–163, 2001] for obtaining coinductive solutions of equations on infinite terms is a special case of a more general recent approach of [F. Bartels. On generalised coinduction and probabilistic specification formats. Distributive laws in coalgebraic modelling. PhD thesis, Free Univ. Amsterdam, 2004. http://homepages.cwi.nl/~bartels/] using distributive laws.

C *-algebras form rather general and rich mathematical structures that can be studied with different morphisms (preserving multiplication, or not), and with different properties (commutative, or not). These various options can be used to incorporate various styles of computation (set-theoretic, probabilistic, quantum) inside categories of C *-algebras. This paper concentrates on the commutative case and shows that there are functors from several Kleisli categories, of monads that are relevant to model probabilistic computations, to categories of C *-algebras. This yields a new probabilistic version of Gelfand duality, involving the “Radon” monad on the category of compact Hausdorff spaces. We also show that a commutative C *-algebra is isomorphic to the space of convex continuous functionals from its state space to the complex numbers. This allows us to obtain an appropriately commuting state-and-effect triangle for commutative C *-algebras.

In automata theory, a machine transitions from one state to the next when it reads an input symbol. It is common to also allow an automaton to transition without input, via an e-transition. These e-transitions are convenient, e.g., when one defines the composition of automata. However, they are not necessary, and can be eliminated. Such e-elimination procedures have been studied separately for different types of automata, including non-deterministic and weighted automata.

The paper has two main parts: First we make the connection between monotone modal logic and the general theory of coalgebras precise by defining functors UpP:Set→Set and UpV:Stone→Stone such that UpP- and UpV-coalgebras correspond to monotone neighbourhood frames and descriptive general monotone frames, respectively. Then we investigate the relationship between the coalgebraic notions of equivalence and monotone bisimulation. In particular, we show that the UpP-functor does not preserve weak pullbacks, and we prove interpolation for a number of monotone modal logics using results on UpP-bisimulations.

Scade is an industrial strength synchronous language and tool suite for the development of the software of safety-critical systems. It supports formal verification using the so-called Design Verifier. Here we start developing a freely available alternative to the Design Verifier intended to support the academic study of verification techniques tailored for SCADE programs. Inspired by work of Hagen and Tinelli on the SMT-based verification of LUSTRE programs, we develop an SMT-based verification method for Scade programs. We introduce Lama as an intermediate language into which Scade programs can be translated and which easily can be transformed into SMT solver instances. We also present first experimental results of our approach using the SMT solver Z3.

Contains fulltext : 132906.pdf (Author’s version preprint ) (Closed access)

Part 2: Regular Contributions; International audience; We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or ϵ -transitions. Our approach employs monads with a parametrized fixpoint operator † to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems.

Distributive laws of a monad over a functor F are categorical tools for specifying algebra-coalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of well-behaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If is a free monad, then such distributive laws correspond to simple natural transformations. However, when is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation from a distributive law for the underlying free monad. We apply this result to show the equivalence between two different representations of context-free languages. © 2013 Springer-Verlag Berlin Heidelberg.

We present a simple tool in Haskell, QStream, implementing the technique of coinductive counting by making use of Haskell's built-in coinduction capabilities. We furthermore provide a number of useful tools for stream exploration, including a number of pretty print functions and integration with the Online Encyclopedia of Integer Sequences.

In the field of structural operational semantics (SOS), there have been several proposals both for syntactic rule formats guaranteeing the validity of algebraic laws, and for algorithms for automatically generating ground-complete axiomatizations. However, there has been no synergy between these two types of results. This paper takes the first steps in marrying these two areas of research in the meta-theory of SOS and shows that taking algebraic laws into account in the mechanical generation of axiomatizations results in simpler axiomatizations. The proposed theory is applied to a paradigmatic example from the literature, showing that, in this case, the generated axiomatization coincides with a classic hand-crafted one. © 2013 Springer-Verlag Berlin Heidelberg. Meta-theory of Algebraic Process Theories Extending and Axiomatizing Structural Operational Semantics: Theory and Tools