Journal Articles

Silva A, Jacobs B, Sokolova A.  2015.  Trace semantics via determinization. Journal of Computer and System Sciences . 81(5):859--879. Abstractdeterminization.pdf

This paper takes a fresh look at the topic of trace semantics in the theory of coalgebras. The first development of coalgebraic trace semantics used final coalgebras in Kleisli categories, stemming from an initial algebra in the underlying category. This approach requires some non-trivial assumptions, like dcpo enrichment, which do not always hold, even in cases where one can reasonably speak of traces (like for weighted automata). More recently, it has been noticed that trace semantics can also arise by first performing a determinization construction. In this paper, we develop a systematic approach, in which the two approaches correspond to different orders of composing a functor and a monad, and accordingly, to different distributive laws. The relevant final coalgebra that gives rise to trace semantics does not live in a Kleisli category, but more generally, in a category of Eilenberg-Moore algebras. In order to exploit its finality, we identify an extension operation, that changes the state space of a coalgebra into a free algebra, which abstractly captures determinization of automata. Notably, we show that the two different views on trace semantics are equivalent, in the examples where both approaches are applicable.

Oliveira N, Silva A, Barbosa LS.  2015.  IMCReo: interactive Markov chains for Stochastic Reo. Journal of Internet Services and Information Security (JISIS). 5(1):3-28.osb15.pdf
Silva A, Jacobs B, Staton S.  2014.  Preface. Electronic Notes in Theoretical Computer Science. 308:1-2. Abstract1-s2.0-s1571066114000681-main.pdf

This volume collects papers presented at the 30th Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXX), held on the campus of Cornell University, Ithaca, New York, USA, from Thursday, June 12 through Sunday, June 15, 2014. The MFPS conferences are devoted to those areas of mathematics, logic, and computer science that are related to models of computation in general and to the semantics of programming languages in particular. The series particularly stresses providing a forum where researchers in mathematics and computer science can meet and exchange ideas about problems of common interest. As the series also strives to maintain breadth in its scope, the conference strongly encourages participation by researchers in neighboring areas.

Silva A, Moon Y-J, Krause C, Arbab F.  2014.  A Compositional Model to Reason About End- to- End QoS in Stochastic Reo Connectors. Science of Computer Programming. 80:3-24. Abstract1-s2.0-s0167642311002073-main.pdf

In this paper, we present a compositional semantics for the channel-based coordination language Reo that enables the analysis of quality of service (QoS) properties of service compositions. For this purpose, we annotate Reo channels with stochastic delay rates and explicitly model data-arrival rates at the boundary of a connector, to capture its interaction with the services that comprise its environment. We propose Stochastic Reo Automata as an extension of Reo automata, in order to compositionally derive a QoS-aware semantics for Reo. We further present a translation of Stochastic Reo Automata to Continuous-Time Markov Chains (CTMCs). This translation enables us to use third-party CTMC verification tools to do an end-to-end performance analysis of service compositions. In addition, we discuss to what extent Interactive Markov Chains (IMCs) can serve as an alternative semantic model for Stochastic Reo. We show that the semantics of Stochastic Reo cannot be specified compositionally using the product operator provided by IMCs.

Silva A, Bonchi F, Bonsangue M, Hansen HH, Panangaen P, Rutten J.  2014.  Algebra- Coalgebra Duality in Brzozowski's Minimization Algorithm. ACM Transactions on Computacional Logic. 15(1):1-29. Abstractbonchi_algebra.pdf

Duality plays a fundamental role in many areas of mathematics, computer science, systems
theory and even physics. For example, the familiar concept of Fourier transform is essentially a duality result: an instance of Pontryagin duality, see, for example the standard textbook [Rudin 1962]. Another basic instance, known to undergraduates, is the duality of a finite-dimensional vector spaces V over some field k, and the space of linear maps from V to k, which is itself a finite-dimensional vector space. Building on this self-duality, a fundamental principle in systems theory due to [Kalman 1959] captures the duality between the concepts of observability and controllability (to be explained below). The latter was further extended to automata theory (where controllability amounts to reachability) in [Arbib and Zeiger 1969], and in various papers [Arbib and Manes 1974; 1975a; 1975c; 1975b; 1980a; 1980b] where Arbib and Manes explored algebraic automata theory in a categorical framework; see also the excellent collection of papers [Kalman et al. 1969] where both automata theory and systems theory is presented.

Silva A, Bonchi F, Bonsangue M, Rutten J.  2013.  Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science. 9(1):1-23. Abstract1302.1046v2_1.pdf

The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence (~_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. We give several examples of applications of our generalized determinization construction, including partial Mealy machines, (structured) Moore automata, Rabin probabilistic automata, and, somewhat surprisingly, even pushdown automata. To further witness the generality of the approach we show how to characterize coalgebraically several equivalences which have been object of interest in the concurrency community, such as failure or ready semantics. .

Bonsangue M, Milius S, Silva A.  2013.  Sound and complete axiomatizations of coalgebraic language equivalence. ACM Transactions on Computational Logic (TOCL). 14(1):1-51. Abstract1104.2803v4.pdf

Coalgebras provide a uniform framework for studying dynamical systems, including several types of automata. In this article, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalized powerset construction that determinizes coalgebras. We show that soundness and completeness are established by proving that expressions modulo axioms of a calculus form the rational fixpoint of the given type functor. Our main result is that the rational fixpoint of the functor FT, where T is a monad describing the branching of the systems (e.g., non-determinism, weights, probability, etc.), has as a quotient the rational fixpoint of the determinized type functor F, a lifting of F to the category of T-algebras. We apply our framework to the concrete example of weighted automata, for which we present a new sound and complete calculus for weighted language equivalence. As a special case, we obtain nondeterministic automata in which we recover Rabinovich’s sound and complete calculus for language equivalence.

Kozen D, Silva A.  2013.  On Moessner's theorem. American Mathematical Monthly. 120(2):131–139. Abstractmoessner.pdf

Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1n, 2n, 3n, ... Paasche's theorem is a generalization of Moessner's; by varying the parameters of the procedure, one can obtain the sequence of factorials 1!, 2!, 3!, ... or the sequence of superfactorials 1!!, 2!!, 3!!, ... Long's theorem generalizes Moessner's in another direction, providing a procedure to generate the sequence a1n-1, (a+d)2n-1, (a+2d)3n-1, ... Proofs of these results in the literature are typically based on combinatorics of binomial coefficients or calculational scans. In this note we give a short and revealing algebraic proof of a general theorem that contains Moessner's, Paasche's, and Long's as special cases. We also prove a generalization that gives new Moessner-type theorems.

Bonchi F, Bonsangue M, Boreale M, Rutten J, Silva A.  2012.  A coalgebraic perspective on linear weighted automata. Information and Computation. 211(1):77–105. Abstractic-lwa.pdf

Weighted automata are a generalisation of non-deterministic automata where each transition, in addition to an input letter, has also a quantity expressing the weight (e.g. cost or probability) of its execution. As for non-deterministic automata, their behaviours can be expressed in terms of either (weighted) bisimilarity or (weighted) language equivalence.

Coalgebras provide a categorical framework for the uniform study of state-based systems and their behaviours. In this work, we show that coalgebras can suitably model weighted automata in two different ways: coalgebras on Set (the category of sets and functions) characterise weighted bisimilarity, while coalgebras on Vect (the category of vector spaces and linear maps) characterise weighted language equivalence.

Relying on the second characterisation, we show three different procedures for computing weighted language equivalence. The first one consists in a generalisation of the usual partition refinement algorithm for ordinary automata. The second one is the backward version of the first one. The third procedure relies on a syntactic representation of rational weighted languages.

Bonsangue M, Clarke D, Silva A.  2012.  A model of context-dependent component connectors. Science of Computer Programming. 77(6):685–706. Abstract14628d_1.pdf

Recent approaches to component-based software engineering employ coordinat- ing connectors to compose components into software systems. For maximum flexibility and reuse, such connectors can themselves be composed, resulting in an expressive calculus of connectors whose semantics encompasses complex combinations of synchronisation, mutual exclusion, non-deterministic choice and state-dependent behaviour. A more expressive notion of connector includes also context-dependent behaviour, namely, whenever the choices a connector can take change non-monotonically as the context, given by the pending activity on its ports, changes. Context dependency can express notions of priority and inhibition. Capturing context-dependent behaviour in formal models is non-trivial, as it is unclear how to propagate context information through composition. In this paper we present an intuitive automata-based formal model of context- dependent connectors, and argue that it is superior to previous attempts at such a model for the coordination language Reo.

Silva A, Bonchi F, Bonsangue M, Rutten J.  2011.  Quantitative Kleene coalgebras. Information and Computation. 209(5):822–849. Abstractic-concur.pdf

We present a systematic way to generate (1) languages of (generalised) regular expressions, and (2) sound and complete axiomatizations thereof, for a wide variety of quantitative systems. Our quantitative systems include weighted versions of automata and transition systems, in which transitions are assigned a value in a monoid that represents cost, duration, probability, etc. Such systems are represented as coalgebras and (1) and (2) above are derived in a modular fashion from the underlying (functor) type of these coalgebras. In previous work, we applied a similar approach to a class of systems (without weights) that generalizes both the results of Kleene (on rational languages and DFA’s) and Milner (on regular behaviours and finite LTS’s), and includes many other systems such as Mealy and Moore machines.

In the present paper, we extend this framework to deal with quantitative systems. As a consequence, our results now include languages and axiomatizations, both existing and new ones, for many different kinds of probabilistic systems.

Silva A, Bonsangue M, Rutten J.  2010.  Non-deterministic Kleene Coalgebras. Logical Methods in Computer Science. 6(3):1–39. Abstract1007.3769.pdf

In this paper, we present a systematic way of deriving (1) languages of (generalized) regular expressions, and (2) sound and complete axiomatizations thereof, for a wide variety of systems. This generalizes both the results of Kleene (on regular languages and deterministic finite automata) and Milner (on regular behaviours and finite labelled transition systems), and includes many other systems such as Mealy and Moore machines.

Silva A, Rutten J.  2010.  A coinductive calculus of binary trees. Information and Computation. 208(5):578–593. Abstract2010-rutten-silva-ic.pdf

We study the set TA of infinite binary trees with nodes labelled in a semiring A from a coalgebraic perspective. We present coinductive definition and proof principles based on the fact that TA carries a final coalgebra structure. By viewing trees as formal power series, we develop a calculus where definitions are presented as behavioural differential equations. We present a general format for these equations that guarantees the existence and uniqueness of solutions. Although technically not very difficult, the resulting framework has surprisingly nice applications, which is illustrated by various concrete examples.