In the setting of (nondeterministic) labeled transition systems, Turi and Plotkin [1] found that GSOS rules essentially correspond to natural transformations of a certain type, which they call abstract GSOS. Those in turn correspond to distributive laws of a monad over a copointed functor as Lenisa, Power, and Watanabe [2 …
read moreFrom Coalgebras to (labeled) transition systems.
For a specific coalgebra one often uses an (ad hoc) transition notation `x -> y', possibly with labels. This talk will discuss a uniform way to associate such a transition relation with a coalgebra, of a polynomial functor F over Sets. More precisely, it will introduce a canonical functor
read moreCoAlg(F …Modeling infinite probabilistic choices using an ultrametric version of kernels
Joint work with Erik de Vink (University of Eindhoven)
In this presentation the applicability of an ultrametric version of stochastic kernels, which extend the notion of compact support measures, is studied in the context of a language with random assignment. In the random assignment the value assigned to a variable …
read moreBeyond Mu-Calculus: strong logics for strong bisimulation
In dealing with transition systems, it is natural to look for logics having the following desirable properties: (1) invariance under (strong) bisimulation (i.e. truth of formulas is preserved by strong bisimulation); (2) decidability.
Standard modal logic and some of its important extensions (logic with star-diamonds for the transitive closure …
read moreCoinductive counting with weighted automata and continued fractions - part 1
We shall elaborate on Sections 13-17 of the recently appeared CWI report
Elements of stream calculus (an extensive exercise in coinduction) SEN-R0120
by treating a number of additional examples of what could be called `coinductive counting'.
The main ideas are to enumerate the structures to be counted (such as binary …
read moreCoordination of Mobile Components
In this talk, we present Reo, a paradigm for composition of software components based on the notion of mobile channels. Both components and channels are mobile in Reo, in the sense that (1) components can move at any time from one location to another, retaining their existing channel links, and …
read moreRecent trends in object oriented verification
I'll discuss an assertional proof method for reasoning about the multi-threaded flow of control in Java. This method combines in a modular manner two well-known proof-methods: the Owicki-Gries method for shared-variable concurrency and the Apt-Francez- de Roever method for CSP.
read moreAxiomatizing GSOS with termination
Aceto, Bloom and Vaandrager showed for the GSOS-format how to generate sound and complete axiomatizations. We add to the GSOS-format a notion of termination and adapt the axiomatization technique for this setting. The result is twofold: successful termination and deadlock are treated separately; the resulting axiom systems are in several …
read moreRho: A Channel-based Coordination Paradigm for Mobile Components
In this talk we present Rho, a paradigm for composition of software components based on the notion of mobile channels. The coordination in Rho is in the same style as in the IWIM model. However, the main focus of attention in Rho is the channels and operations on them, not …
read moreShared Data Space Systems: Verification and Expressiveness Results
In shared data space architectures, several applications coordinate by reading and writing to a common data store. In this talk we view the data space as a separate process. We show how a number of variants of shared data space architectures can be easily modeled in muCRL, at various levels …
read more