Conference Papers

Silva A, Bonchi F, Milius S, Zanasi F.  2014.  How to Kill Epsilons with a Dagger - A Coalgebraic Take on Systems with Algebraic Label Structure. 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.  Towards a Coalgebraic Chomsky Hierarchy. 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.  Quantitative Analysis of Reo- Based Service Coordination. 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.  Language Constructs for Non-Well-Founded Computations. 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.  A coalgebraic view of e- transitions. 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.  Brzozowski's and up to algorithms for must testing. 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.  Left-handed completeness. 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.  Trace Semantics via Determinization. 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.

Bonchi F, Bonsangue M, Caltais G, Rutten J, Silva A.  2012.  Final semantics for decorated traces. 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.

Adámek J, Bonchi F, Hülsbusch M, König B, Milius S, Silva A.  2012.  A coalgebraic perspective on minimization and determinization. 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.

Moon Y-J, Arbab F, Silva A, Stam A, Verhoef C.  2011.  Stochastic Reo: a case study. 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.  A Specification Language for Reo Connectors. 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.

Silva A, Sokolova A.  2011.  Sound and Complete Axiomatization of Trace Semantics for Probabilistic Systems. Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS '11). 276:291––311. Abstractbms-11-draft.pdf

Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, 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 generalised powerset construction. We illustrate the framework with two examples: non-deterministic automata, for which we recover Rabinovich’s sound and complete calculus for language equivalence, and weighted automata, for which we present the first sound and complete calculus for weighted language equivalence.

Silva A, Bonchi F, Bonsangue M, Rutten J.  2010.  Generalizing the powerset construction, coalgebraically. Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). 8:272–283. Abstract24.pdf

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 behavioral equivalence ($\sim_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. The powerset construction is a standard method for converting a nondeterministic automaton into an equivalent deterministic one as far as language is concerned. In this paper, we lift the powerset construction on automata to the more general framework of coalgebras with structured state spaces. Examples of applications include partial Mealy machines, (structured) Moore automata, and Rabin probabilistic automata.

Bonsangue M, Caltais G, Goriac E, Lucanu D, Rutten J, Silva A.  2010.  A decision procedure for bisimilarity of generalized regular expressions. Proceedings of the 13th Brazilian Symposium on Formal Methods (SBMF 2010). 6527:226–241. Abstractsbmf10.pdf

A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analogue of Kleene’s theorem and Kleene algebra, were recently proposed by a subset of the authors of this paper. Examples of the systems covered include infinite streams, deterministic automata and Mealy machines. In this paper, we present a tool where the aforementioned expressions can be derived automatically and a novel algorithm to decide whether two expressions are bisimilar or not. The procedure is implemented in the automatic theorem prover CIRC, by reducing coinduction to an entailment relation between an algebraic specification and an appropriate set of equations.

Moon Y-J, Silva A, Krause C, Arbab F.  2010.  A Compositional Semantics for Stochastic Reo Connectors. Proceedings of the 9th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA '10). 30:93–107. Abstract16529d.pdf

In this paper we present a compositional semantics for the channel-based coordination language Reo which 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.

Bonchi F, Bonsangue M, Rutten J, Silva A.  2009.  Deriving Syntax and axioms for quantitative regular behaviours. Proceedings of the 20th International Conference on Concurrency Theory (CONCUR 2009). 5710:146–162. Abstractconcur09.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.

Bonsangue M, Clarke D, Silva A.  2009.  Automata for Context-dependent Connectors. Proceedings of the Eleventh International Conference on Coordination Models and Languages (Coordination 2009). 5521:184–203. Abstractcoord09.pdf

Recent approaches to component-based software engineering employ coordinating 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 the 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 in- formation 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.

Bonsangue M, Rutten J, Silva A.  2009.  A Kleene theorem for polynomial coalgebras. Proceedings of the Twelfth International Conference on Foundations of Software Science and Computation structures (FoSSaCS 2009). 5504:122–136. Abstractbrs09a.pdf

For polynomial functors G, we show how to generalize the classical notion of regular expression to G-coalgebras. We introduce a language of expressions for describing elements of the final G-coalgebra and, analogously to Kleene’s theorem, we show the correspondence between expressions and finite G-coalgebras.

Barbosa LS, Oliveira JN, Silva A.  2008.  Calculating invariants as coreflexive bisimulations. Proceedings of 12th International Conference on Algebraic Methodology and Software Technology - AMAST . 5140:83–99. Abstractamast08-bos.pdf

Invariants, bisimulations and assertions are the main ingredients of coalgebra theory applied to software systems. In this paper we reduce the first to a particular case of the second and show how both together pave the way to a theory of coalgebras which regards invariant predicates as types. An outcome of such a theory is a calculus of invariants’ proof obligation discharge, a fragment of which is presented in the paper.The approach has two main ingredients: one is that of adopting relations as “first class citizens” in a pointfree reasoning style; the other lies on a synergy found between a relational construct, Reynolds’ relation on functions involved in the abstraction theorem on parametric polymorphism and the coalgebraic account of bisimulations and invariants. This leads to an elegant proof of the equivalence between two different definitions of bisimulation found in coalgebra literature (due to B. Jacobs and Aczel & Mendler, respectively) and to their instantiation to the classical Park-Milner definition popular in process algebra.

Bonsangue M, Rutten J, Silva A.  2008.  Coalgebraic logic and synthesis of mealy machines. Proceedings of the Eleventh International Conference on Foundations of Software Science and Computation structures (FoSSaCS 2008). 4962:231–245. Abstractmealy.pdf

We present a novel coalgebraic logic for deterministic Mealy machines that is sound, complete and expressive w.r.t. bisimulation. Every finite Mealy machine corresponds to a finite formula in the language. For the converse, we give a compositional synthesis algorithm which transforms every formula into a finite Mealy machine whose behaviour is exactly the set of causal functions satisfying the formula.

Silva A, Rutten J.  2007.  Behavioural differential equations and coinduction for binary trees. Proceedings of the Workshop on Logic, Language, Information and Computation 2007 (WoLLIC 2007). 4576:322–336. Abstractwollic2007.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.

Silva A, Visser J.  2006.  Strong types for relational databases. Proceedings of the 2006 ACM SIGPLAN workshop on Haskell (Haskell '06). :25–36. Abstracthw2006.pdf

Haskell's type system with multi-parameter constructor classes and functional dependencies allows static (compile-time) computations to be expressed by logic programming on the level of types. This emergent capability has been exploited for instance to model arbitrary-length tuples (heterogeneous lists), extensible records, functions with variable length argument lists, and (homogenous) lists of statically fixed length (vectors).We explain how type-level programming can be exploited to define a strongly-typed model of relational databases and operations on them. In particular, we present a strongly typed embedding of a significant subset of SQL in Haskell. In this model, meta-data is represented by type-level entities that guard the semantic correctness of database operations at compile time.Apart from the standard relational database operations, such as selection and join, we model functional dependencies (among table attributes), normal forms, and operations for database transformation. We show how functional dependency information can be represented at the type level, and can be transported through operations. This means that type inference statically computes functional dependencies on the result from those on the arguments.Our model shows that Haskell can be used to design and prototype typed languages for designing, programming, and transforming relational databases.