Search

Reo is a visual language of connectors that originated in component-based software engineering. It is a flexible and intuitive language, yet powerful and capable of expressing complex patterns of composition. The intricacies of the language resulted in many semantic models proposed for Reo, including several automata-based ones.

Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics., Comment: Accepted at MPC 2019

Domain Specific Languages (DSLs) provide a lightweight approach to incorporate formal techniques into the industrial workflow. From DSL instances, formal models and other artefacts can be generated, such as simulation models and code. Having a single source for all artefacts improves maintenance and offers a high return on investment of the initial modelling effort. Since DSLs can be used to capture essential domain information at a high level of abstraction, this supports formal verification early in the development process. We discuss our experiences with this approach in a number of real industrial development projects. cop. Springer International Publishing Switzerland 2016.

Contains fulltext : 159576.pdf (Author’s version preprint ) (Open Access)

In this paper we concern ourselves with normative multi-agent systems, which are multi-agent systems governed by a set of norms. In these systems, the internals and architecture of the participating agents may be unknown to us, which disables us to make any strong assumption on the possible behaviour that these agents may exhibit. Thus, we cannot simply assume that the agents are aware of the norms, or that they are compliant with respect to the norms. In other words, a crucial problem that needs to be solved is how we can verify these systems if we have no idea whether the agents will be norm-obedient. This paper investigates two distinct formal frameworks which allow us to tackle this problem, namely in the first part of this paper we propose a logic-based framework which uses compliance types, and in the second part we propose a framework which tackles the problem from a mechanism-design perspective.

Contains fulltext : 34595.pdf (Author’s version preprint ) (Open Access)

We study weighted automata from both an algebraic and a coalgebraic perspective. In particular, we consider equations and coequations for weighted automata. We prove a duality result that relates sets of equations (congruences) with (certain) subsets of coequations. As a consequence, we obtain two equivalent but complementary ways to define classes of weighted automata. We show that this duality cannot be generalized to linear congruences in general but we obtain partial results when weights are from a field.

This paper introduces a coalgebraic foundation for coinductive types, interpreted as sets of values and extended with set theoretic union. We give a sound and complete characterization of semantic subtyping in terms of inclusion of maximal traces. Further, we provide a technique for reducing subtyping to inclusion between sets of finite traces, based on approximation. We obtain inclusion of tree languages as a sound and complete method to show semantic subtyping of recursive types with basic types, product and union, interpreted coinductively.

Item does not contain fulltext

Bisimulation-up-to enhances the bisimulation proof method for process equivalence. We present its generalization from labelled transition systems to arbitrary coalgebras, and show that for a large class of systems, enhancements such as bisimulation up to bisimilarity, up to equivalence and up to context are sound proof techniques. This allows for simplified bisimulation proofs for many different types of state-based systems.

Language equivalence can be checked coinductively by establishing a bisimulation on suitable deterministic automata. We improve and extend this technique with bisimulation-up-to, which is an enhancement of the bisimulation proof method. First, we focus on the regular operations of union, concatenation and Kleene star, and illustrate our method with new proofs of classical results such as Arden’s rule. Then we extend our enhanced proof method to incorporate language complement and intersection. Finally we define a general format of behavioural differential equations, in which one can define operations on languages for which bisimulation-up-to is a sound proof technique.

In this paper we present a coinductive definition of context free power series in terms of behavioural differential equations. We show that our coalgebraic approach provides a unified view on many, at first sight different, existing notions of algebraicity, and we apply our behavioural differential equations to produce a new proof for a classical result by Chomsky and Schutzenberger, and a simple proof that the zip-operator of two algebraic streams is algebraic.

International audience; 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.

We give a coalgebraic account of context-free languages using the functor D(X) = 2 × XA for deterministic automata over an alphabet A, in three different but equivalent ways: (i) by viewing context-free grammars as D-coalgebras; (ii) by defining a format for behavioural differential equations (w.r.t. D) for which the unique solutions are precisely the context-free languages; and (iii) as the D-coalgebra of generalized regular expressions in which the Kleene star is replaced by a unique fixed point operator. In all cases, semantics is defined by the unique homomorphism into the final coalgebra of all languages, paving the way for coinductive proofs of context-free language equivalence. Furthermore, the three characterizations can serve as the basis for the definition of a general coalgebraic notion of context-freeness, which we see as the ultimate long-term goal of the present study.

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 novel algorithm and a tool 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. published

Contains fulltext : 286126.pdf (Publisher’s version ) (Open Access) 29 p.

A coherent description of architectures provides insight, enables communication among different stakeholders and guides complicated (business and ICT) change processes. Unfortunately, so far no architecture description language exists that fully enables integrated enterprise modeling. In this paper we focus on the requirements and design of such a language. This language defines generic, organization-independent concepts that can be specialized or composed to obtain more specific concepts to be used within a particular organisation. It is not our intention to re-invent the wheel for each architectural domain: wherever possible we conform to existing languages or standards such as UML. We complement them with missing concepts, focusing on concepts to model the relationships among architectural domains. The concepts should also make it possible to define links between models in other languages. The relationship between architecture descriptions at the business layer and at the application layer (business-IT alignment) plays a central role.