We present a proof-technique for reducing the nondeterminism of abstract agent specifications by means of refinement. We implement the operational semantics of agent specifications in rewrite systems, such that we can automatically check if refinement between (fair) executions of agents holds.
read moreReo Meets Real World: Coordination at your Service.
This talk addresses the issues of service coordination in complex business process scenarios. While existing approaches for service coordination, e.g., BPEL are powerful standards for composition of services, they lack support for a number of features highly desirable for service coordination, e.g., they hard-wire services too much, or …
read moreFlat modal fixpoint logics
Modal fixpoint logics constitute a research field of considerable interest, not only because of its many applications in computer science, but also because of its rich mathematical theory, which features connections with fields as diverse as lattice theory, automata theory, and universal coalgebra.
In this talk I discuss so-called flat …
read moreCoalgebras and their types
The theory of Universal Coalgebra, pioneered by Jan Rutten (CWI), offers a unified framework for studying diverse types of state based systems, useful in stream programming, object oriented programming, automata theory, Kripke Structures, probabilistic transition systems, and even topological spaces. The type of a coalgebra is determined by the choice …
read moreTowards Distributed Reo
Various semantic models exist to formalize Reo, each serving a different purpose. In this work we mainly focus on formal models suitable for deriving a distributed implementation.
For our implementation platform, we assume a distributed environment where each (distributed) element knows about its own neighbors only. We propose an executable …
read moreSynthesis of Connectors from Scenario-based Interaction Specifications
The idea of synthesizing state-based models from scenario-based interaction specifications has received much attention in recent years. The synthesis approach not only helps to significantly reduce the effort of system construction, but it also provides a bridge over the gap between requirements and implementation of systems. However, the existing synthesis …
read moreAn information-theoretic framework for anonymity and the problem of non-determinism.
This talk is composed by two fairly independent but related parts. In the first part I will make a brief introduction to the problem of anonymity. Then I will introduce an information-theoretic framework in which these protocols are interpreted as noisy channels, and I will discuss various quantitative definitions of …
read moreDiscrete dualities for contexts and concepts from formal concept analysis
This is joint work with Prof Ewa Orlowska, National Insitute of Telecommunications, Warsaw. In this talk we show that the fundamental notions of formal concept analysis, namely contexts and concepts, can be studied within the framework of discrete dualities. For contexts we define a class of context algebras and establish …
read moreSubsequential Transducers and Coalgebra
Subsequential transducers are deterministic finite state machines which compute partial word functions f: A^ --> B^. They have applications in coding theory and language processing, and they generalise both deterministic finite automata (DFAs) and Mealy machines. It is known that DFAs and Mealy machines can be viewed as coalgebras such that …
read moreBisimulations for neighbourhood structures (Part 2)
Neighbourhood semantics forms a generalisation of Kripke semantics, and it has become the standard tool for reasoning about non-normal modal logics in which (Kripke valid) principles such as []p /\ []q (Meet) and []p -> (Mon) are considered not to hold. In computer science and social choice theory, non-normal modal logics are …
read more