Publications

Bonchi F, Bonsangue M, Rutten J, Silva A.  2012.  Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday. 7230:12–23. AbstractWebsite

We give a new presentation of Brzozowski’s algorithm to minimize finite automata, using elementary facts from universal algebra and coalgebra, and building on earlier work by Arbib and Manes on the duality between reachability and observability. This leads to a simple proof of its correctness and opens the door to further generalizations.

Silva A, Jacobs B.  2014.  Categories and Types in Logic, Language, and Physics - Lecture Notes in Computer Science. 8222:211-234. Abstract

One of the many results which makes Joachim Lambek famous is: an initial algebra of an endofunctor is an isomorphism. This fixed point result is often referred to as Lambek's Lemma''. In this paper, we illustrate the power of initiality by exploiting it in categories of algebra-valued presheaves $\EM(T)^{\N}$, for a monad $T$ on $\Sets$.
The use of presheaves to obtain certain calculi of expressions (with variable binding) was introduced by Fiore, Plotkin, and Turi. They used set-valued presheaves, whereas here the presheaves take values in a category $\EM(T)$ of Eilenberg-Moore algebras. This generalisation allows us to develop a theory where more structured calculi can be obtained. The use of algebras means also that we work in a linear context and need a separate operation $\bang$ for replication, for instance to describe strength for an endofunctor on $\EM(T)$. We apply the resulting theory to give systematic descriptions of non-trivial calculi: we introduce non-deterministic and weighted lambda terms and expressions for automata as initial algebras, and we formalise relevant equations diagrammatically.

Silva A, Jacobs B.  2014.  Horizons of the Mind. A Tribute to Prakash Panangaden - Lecture Notes in Computer Science. 8464 Abstract

Automata learning is a known technique to infer a finite state machine from a set of observations. In this paper, we revisit Angluin’s original algorithm from a categorical perspective. This abstract view on the main ingredients of the algorithm lays a uniform framework to derive algorithms for other types of automata. We show a straightforward generalization to Moore and Mealy machines, which yields an algorithm already know in the literature, and we discuss generalizations to other types of automata, including weighted automata.

Silva A, Bonchi F, Milius S, Zanasi F.  2014.  CMCS -55th Annual Mathematics Conference. 8446 Abstract1402.4062v2.pdf

We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or \epsilon-transitions. Our approach employs monads with a parametrized fixpoint operator \dagger 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.

Silva A, SergeyGoncharov, Milius S.  2014.  IFIP International Conference on Theoretical Computer Science (IFIP TCS). 8705 Abstract1401.5277v3.pdf

The Chomsky hierarchy plays a prominent role in the foundations of the theoretical computer science relating classes of formal languages of primary importance. In this paper we use recent developments on coalgebraic and monad-based semantics to obtain a generic notion of a T-automaton, where T is a monad, which allows the uniform study of various notions of machines (e.g. finite state machines, multi-stack machines, Turing machines, valence automata, weighted automata). We use the generalized powerset construction to define a generic (trace) semantics for T-automata, and we show by numerous examples that it correctly instantiates for the known classes of machines/languages captured by the Chomsky hierarchy. Moreover, our approach provides new generic techniques for proving expressivity bounds of various machine-based models.

Silva A, Oliveira N, Barbosa LS.  2014.  SAC - 29th Symposium On Applied Computing. Abstractimcreoosb.pdf

Quality of Service analysis of composed software systems is an active research area, with the goal of evaluating and improving performance and resource allocation in serviceoriented applications, namely, in the glue code –coordination layer– of such systems. Stochastic Reo offers constructs for
service coordination and allows the specification of stochastic values for channels. But its state-of-the-art semantic models fail in several (important) ways. In this paper, we will see how Interactive Markov chains (IMC), proposed as astochastic compositional model of concurrency, can be effectively used to serve as a compositional semantic model for Stochastic Reo. Treating IMC as a direct semantic model, gives rise to more faithful models and has obvious efficiency advantages. Moreover, tool support that exists for IMC is made available, without significant effort, to verify and reason about the coordination layer modelled as Reo connectors.

Jeannin J-B, Kozen D, Silva A.  2013.  22nd European Symposium on Programming - ESOP. 7792:61–80. Abstractnwf.pdf

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 epsilon-transition. These epsilon-transitions are convenient, e.g., when one defines the composition of automata. However, they are not necessary, and can be eliminated. Such epsilon-elimination procedures have been studied separately for different types of automata, including non-deterministic and weighted automata. It has been noted by Hasuo that it is possible to give a coalgebraic account of epsilon-elimination for some automata using trace semantics (as defined by Hasuo, Jacobs and Sokolova). In this paper, we give a detailed description of the epsilon-elimination procedure via trace semantics (missing in the literature). We apply this framework to several types of automata, and explore its boundary. In particular, we show that is possible (by careful choice of a monad) to define an epsilon-removal procedure for all weighted automata over the positive reals (and certain other semirings). Our definition extends the recent proposals by Sakarovitch and Lombardy for these semirings.

Silva A, Westerbaan B.  2013.  CALCO - 5th Conference on Algebra and Coalgebra in Computer Science. 8089 Abstractmain.pdf

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 ε-transition. These ε-transitions are convenient, e.g., when one defines the composition of automata. However, they are not necessary, and can be eliminated. Such ε-elimination procedures have been studied separately for different types of automata, including non-deterministic and weighted automata.
It has been noted by Hasuo that it is possible to give a coalgebraic account of ε-elimination for some automata using trace semantics (as defined by Hasuo, Jacobs and Sokolova).
In this paper, we give a detailed description of the ε-elimination procedure via trace semantics (missing in the literature). We apply this framework to several types of automata, and explore its boundary.
In particular, we show that is possible (by careful choice of a monad) to define an ε-removal procedure for all weighted automata over the positive reals (and certain other semirings). Our definition extends the recent proposals by Sakarovitch and Lombardy for these semirings.

Silva A, Pous D, Caltais G, Bonchi F.  2013.  APLAS - 11th Asian Symposium on Programming Languages and Systems. 8301 Abstractaplas13bcps.pdf

Checking language equivalence (or inclusion) of nite automata is a classical problem in Computer Science, which has recently received a renewed interest and found novel and more e ective solutions, such as approaches based on antichains or bisimulations up-to. Several notions of equivalence (or preorder) have been proposed for the analysis of concurrent systems. Usually, the problem of checking these equivalences is reduced to checking bisimilarity. In this paper, we take a di ferent approach and propose to adapt algorithms for language equivalence to check one prime equivalence in concurrency theory, must testing semantics. To achieve this transfer of technology from language to must semantics, we take a coalgebraic outlook at the problem.

Kozen D, Silva A.  2012.  13th International Conference on Relational and Algebraic Methods in Computer Science. 7560:162–178. Abstractleft.pdf

We give a new, significantly shorter proof of the completeness of the left-handed star rule of Kleene algebra. The proof reveals the rich interaction of algebra and coalgebra in the theory.

Jacobs B, Silva A, Sokolova A.  2012.  Proceedings of the 11th International Workshop on Coalgebraic Methods in Computer Science (CMCS 2012). 7399:109–129. 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 (see notably~\cite{HasuoJS07}). 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 (see~\cite{SBBR10}) 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.

Adámek J, Bonchi F, Hülsbusch M, König B, Milius S, Silva A.  2012.  Proceedings of the Fifteenth International Conference on Foundations of Software Science and Computation structures (FoSSaCS 2012). 7213:58–73. Abstractfossacs12-extended.pdf

Coalgebra offers a unified theory of state based systems, including infinite streams, labelled transition systems and deterministic automata. In this paper, we use the coalgebraic view on systems to derive, in a uniform way, abstract procedures for checking behavioural equivalence in coalgebras, which perform (a combination of) minimization and determinization. First, we show that for coalgebras in categories equipped with factorization structures, there exists an abstract procedure for equivalence checking. Then, we consider coalgebras in categories without suitable factorization structures: under certain conditions, it is possible to apply the above procedure after transforming coalgebras with reflections. This transformation can be thought of as some kind of determinization. We will apply our theory to the following examples: conditional transition systems and (non-deterministic) automata.

Bonchi F, Bonsangue M, Caltais G, Rutten J, Silva A.  2012.  Proceedings of the Twenty-eighth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2012). 286:73–86. Abstractdecorated.pdf

In concurrency theory, various semantic equivalences on la- belled transition systems are based on traces enriched or decorated with some additional observations. They are generally referred to as decorated traces, and examples include ready, failure, trace and complete trace equivalence. Using the generalized powerset construction, recently introduced by a subset of the authors (FSTTCS’10), we give a coalgebraic presentation of decorated trace semantics. This yields a uniform notion of canonical, minimal representatives for the various decorated trace equivalences, in terms of final Moore automata. As a consequence, proofs of decorated trace equivalence can be given by coinduction, using different types of (Moore-) bisimulation, which is helpful for automation.

Moon Y-J, Arbab F, Silva A, Stam A, Verhoef C.  2011.  Proceedings of the 5th International Workshop on Harnessing Theories for Tool Support in Software (TTSS '11). Abstractttss11.pdf

QoS analysis of coordinated distributed autonomous services is currently of interest in the area of service-oriented computing and calls for new technologies and supporting tools. In previous work, the first three authors have proposed a compositional automata model to provide semantics for stochastic Reo, a channel based coordination language that supports the specification of QoS values (such as request arrivals or processing rates). Furthermore, translations from this automata model into stochastic models, such as continuous-time Markov chains (CTMCs) and interactive Markov chains (IMCs) have also been presented. Based on those results, we describe in this paper a case study of QoS analysis. We analyze a certain instance of the ASK system, an industrial software system for connecting people offering professional services to clients requiring those services. We develop a model of the ASK system using stochastic Reo. The distributions used in this model were obtained by applying statistical analysis techniques on the raw values that we obtained from the real logs of an actual running ASK system. These distributions are used for the derived CTMC model for the ASK system to analyze and to improve the performance of the system, under the assumption that the distributions are exponentially distributed. In practice, this is not always the case. Thus, we also carry out a simulation-based analysis by a Reo simulator that can deal with non-exponential distributions. Compared to the analysis on the derived CTMC model, the simulation is approximation-based analysis, but it reveals valuable insight in the behavior of the system. The outcome of both analyses helps both the developers and the installations of the ASK system to improve the performance of the system.

Silva A.  2011.  Proceedings of the Fundamentals of Software Engineering - 4th IPM International Conference (FSEN 2011). 7141:368–376. Abstract18033d_2.pdf

Recent approaches to component-based software engineering employ coordinating connectors to compose components into software systems. Reo is a model of component coordination, wherein complex connectors are constructed by composing various types of primitive channels.Reo automata are a simple and intuitive formal model of context- dependent connectors, which provided a compositional semantics for Reo.

In this paper, we study Reo automata from a coalgebraic perspective. This enables us to apply the recently developed coalgebraic theory of generalized regular expressions in order to derive a specification language, tailor-made for Reo automata, and sound and complete axiomatizations with respect to three distinct notions of equivalence: (coalgebraic) bisimilarity, the bisimulation notion studied in the original papers on Reo automata and trace equivalence. The obtained language is simple, but nonetheless expressive enough to specify all possible finite Reo automata. Moreover, it comes equipped with a Kleene-like theorem: we provide algorithms to translate expressions to Reo automata and, conversely, to compute an expression equivalent to a state in a Reo automaton.