The coordination principle is often cited as: separate computation from coordination. I will present a method for the design of parallel programs based on this principle.
This coordination principle can be extrapolated: separate those aspects of a system that can change independently. In the second part of this talk I …
read moreIn previous presentations a notion of probabilistic predicate and a Hoare style logic have been introduced. A basic probabilistic predicate gives the probability of a certain property. The predicates can be combined with both logical operators and arithmetical operators.
In this presentation a language with both nondeterminism and probability is …
read moreAs an extensive exercise in the use of coinductive techniques, the set of all streams (here: infinite sequences of real numbers) is turned into a calculus in two ways:
the operation of `tail' of a stream is taken as a formal notion of derivative: (s0, s1, s2, ...) ' = (s1, s2, s3 …
read moreJoint-work with F. Arbab, M.M. Bonsangue, and F.S. de Boer.
A mobile channel is a link that provides an asynchronous and anonymous means of communication between two components in a distributed system . A channel is called mobile if either of its (channel-)ends can be moved from one …
read moreThe carrier sets of final coalgebras have been shown (amongst others by Jan Rutten) to be a suitable domain to model infinite datatypes or the behaviour of dynamical systems. The basic means to characterise their elements (also called states here) is the coiteration schema, which is directly related to the …
read moreI am reintroducing a modal logic of epistemic actions (some versions of which were already presented at previous ACG meetings) and exploring its applications to discrete-event control problems with decentralized supervisors, who can only partially observe events but who may be able to communicate with each other.
The idea to …
read moreJoint work with J.N. Kok
A type theory with infinitary intersection and union types for the lazy lambda calculus is introduced. The meaning of types are subsets of a universe of discourse. Intersection and union type constructors are interpreted as the set-theoretic intersection and union, respectively, even when they …
read moreCoalgebras for a functor on the category of sets subsume many formulations of the notion of transition system, including labelled transition systems, Kripke models, Kripke frames and many types of automata. The talk presents a multimodal language which is bisimulation invariant and (under a natural completeness condition) expressive enough to …
read moreA classical problem in distributed systems is detecting the termination of a distributed computation. Distributed Termination Detection (DTD) has been extensively studied in the past twenty years and it is known to be a difficult problem to solve efficiently, because it involves properties of the global state of a distributed …
read moreThe majority of the verification methods for software systems only
produce qualitative information. Questions like Does the system
satisfy the specification?'' andAre the systems semantically
equivalent?'' are answered. However, this information is often too
restrictive in practice and a (complementary) quantitative approach to
verification is needed. For example, answers …