I introduce a notion of (discrete) probabilistic epistemic process and an associated dynamic-epistemic modal logic. I use them to redefine and analize some notions of game theory: extensive games with imperfect information, perfect recall, mixed strategies, beliefs about strategies, epistemic types, Bayesian belief-revision, rationality and rationalizability, solution concepts.

read more# On the Duality of Modal and Equational Logic

Basic notions of coalgebras and modal logic are reviewed.

A categorical description of coalgebraic semantics of modal logics is developed.

This description turns out to dualise algebraic semantics of equational logic as given by Banaschewski and Herrlich in the paper "Subcategories defined by implications" (1976). This gives a precise meaning …

read more# On the Duality of Observability and Reachability

Joint work with Rolf Hennicker (University of Munich) and Michel Bidoit (Ecole Normale Sup351rieure de Cachan).

The properties of a system being "observable" or "fully abstract" (all internal states can be distinguished by an external observer) and of being "reachable" (all internal states are relevant, i.e., can be reached …

read more# A logical interface description language for components

Joint work with F. Arbab and F. de Boer

We present a formal model for component-based system, a logic based interface description language that conveys the observable semantics of a component, and a formal system for deriving properties of the system out of the interface of each of its constituent …

read more# Back To The Future: A Family of DTD Algorithms

We discuss our work-in-progress on a number of Distributed Termination Detection Algorithms. These algorithms use message histories to construct administrative trees called message futures. These algorithms allow generalized network topologies and support dynamic changes to the network. The performance of these algorithms can be optimized with special information about the …

read more# Stream calculus

Exploiting the fact that the set of all streams (infinite sequences of real numbers) carries a final coalgebra structure, a few initial steps towards a coinductive stream calculus are discussed. This involves definitions in terms of behavioural differential equations, methods for solving such equations, and (generalized) nondeterministic representations of such …

read more# Modeling continuous probabilistic choice using stochastic kernels

Joint work with Erik de Vink (at KPN Research by that time)

To model discrete probabilistic choices summation of measures can be used. For continues choices, e.g. selection of a number in [0,1], integration is required. To enable the use of integration, stochastic kernels are introduced. The use …

read more# A Generalized Schema for Coinductive Definitions

For a given behavior type (functor), the carrier of a final coalgebra provides a unique representative for each possible behavior. This property immediately leads to a definition (and proof) principle - called `coiteration' here - for functions from an arbitrary set to this carrier: To define the function's value on a given …

read more# Combinators for hyperedge replacement graph rewriting

GS theories are generalizations of Lawvere's algebraic theories having explicit operations of sharing and garbage collection of 'interfaces'. They have been used to give functorial semantics to term graph rewriting and (for the static aspects) to concurrent and mobility calculi (like asynchronous pi-calculus). A higher order extension of them, called …

read more