Publications

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.

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.

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.

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.

Bliudze S, Bruni R, Bruni R, Carbone M, Silva A.  2012.  Towards Interaction Reliability in Concurrent Applications. Scientific Annals of Computer Science. 22:1-4. Abstractxxii1_0.pdf

Developing trustworthy concurrent applications is a seemingly never ending quest, which is necessary but dicult. It is necessary because mainstream systems and applications are inherently concurrent and they are pervasive to our daily life activities. It is dicult because such systems are inherently interactive and heterogeneous, so that boundaries can hardly be established for studying subsystems in isolation.
Formal methods are a key instrument in resolving ambiguities and design reliable applications in a rigorous way. The authors overview major problems in the application of formal methods and outline how they are tackled by the papers collected in this volume.

Carbone M, Lanese I, Silva A, Sokolova A.  2012.  Proceedings Fifth Interaction and Concurrency Experience. ICE. 104
Constable RL, Silva A.  2012.  Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science. 7230
Mokhtar SB, Bliudze S, Bruni R, Silva A, Troina A.  2011.  Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction {ICE}. 38 Abstractxxi1_6.pdf

The authors emphasize the actual relevance and need of formal methods for the advancements of complex systems, and brie y present the other papers contained in this issue.