Markov Chains are an important class of stochastic processes that are widely used in practice to determine system performance and dependability characteristics. This talk will consider discrete-time and continuous-time Markov chains and explain notions of strong and weak simulation and bisimulation relations for them. Moreover, the talk will discuss the …
read moreRebeca: An Actor-Based Model for Formal Modelling and Verification of Reactive Systems
Object-oriented modelling is known to be an appropriate approach for representing concurrent and distributed systems. Besides having an appropriate and efficient way for modelling these systems, one needs a formal verification approach for ensuring their correctness. Therefore, we have developed an actor-based model for describing such systems.
We use temporal …
read moreA hierarchy of probabilistic system types
Joint work with Erik de Vink (TU/e).
Many approaches in standard concurrency theory are commonly based on labelled transition systems or some minor variant thereof. When probabilities are introduced however, many different system types emerge: some authors for instance consider fully probabilistic systems, while others use systems which incorporate …
read moreA graphical user interface for REO
In this talk I present a Graphical User Interface (GUI) for a simulator of the Coordination Language Reo, implemented in C++ using the Qt graphical libraries.
After briefly recalling some Reo concepts, I summarize the necessary features such a GUI should offer and mark those that are already implemented. I …
read moreInput-output logic
Joint work with David Makinson, King's College London.
Input-output logic (IOL) is a theory of input/output operations resembling inference, but where input propositions are not in general included among outputs, and the operation is not in any way reversible. Examples arise in contexts of conditional obligations, goals, ideals, preferences …
read moreFull Abstraction in Structural Operational Semantics
This talk explores the connection between semantic equivalences for concrete sequential processes, represented by means of transition systems, and formats of transition system specifications using Plotkin's structural approach. For several equivalences in the linear time - branching time spectrum a format is given, as general as possible, such that this equivalence …
read moreA coalgebraic semantics for positive modal logic
Positive Modal Logic (PML) is the logic of Kripke structures in a language containing conjunction, disjunction and modal operators, but no negation or implication. The class of algebras canonically associated with PML forms a category which is dually equivalent to certain topological spaces (Priestley spaces) endowed with relations, which are …
read moreA Hoare Logic for Knowledge Programs
I present some new results and developments of my work on modeling communication and learning in distributed systems.
Epistemic programs are programs for jointly updating all the agents' states of knowledge (or "belief") about the current system. They can be intuitively understood as computing the effect of exchanges of information …
read moreFOLD: first order logic of domains
We introduce an interpretation of domains in terms of a logic including bounded existential and universal quantifiers. The logic is compositional with respect to domain constructors like function space and Plotkin powerdomain, and sound with respect to the ordinary interpreation of domains as some kind of complete partial orders. A …
read moreIntroduction to Presheaves, Open Maps, and Weak Factorisation Systems
Presheaves are widely used as models for concurrency. The aim of the talk is to give an introduction to presheaves and the associated notion of bisimulation called open maps. Mathematically, presheaves are attractive because they are simple (presheaves are just set-valued functors), cover many interesting examples (e.g. unary algebras …
read more