Search

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.

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.

We investigate logics for coalgebraic simulation from a compositional perspective. Specifically, we show that the expressiveness of an inductively-defined language for coalgebras w.r.t. a given notion of simulation comes as a consequence of an expressivity condition between the language constructor used to define the language for coalgebras, and the relator used to define the notion of simulation. This result can be instantiated to obtain Baltag's logics for coalgebraic simulation, as well as a logic which captures simulation on unlabelled probabilistic transition systems. Moreover, our approach is compositional w.r.t. coalgebraic types. This allows us to derive logics which capture other notions of simulation, including trace inclusion on labelled transition systems, and simulation on discrete Markov processes.