This paper investigates stochastic nondeterminism on continuous state spaces by relating nondeterministic kernels and stochastic effectivity functions to each other. Nondeterministic kernels are functions assigning each state a set o subprobability measures, and effectivity functions assign to each state an upper-closed set of subsets of measures. Both concepts are generalizations of Markov kernels used for defining two different models: Nondeterministic labelled Markov processes and stochastic game models, respectively. We show that an effectivity function that maps into principal filters is given by an image-countable nondeterministic kernel, and that image-finite kernels give rise to effectivity functions. We define state bisimilarity for the latter, considering its connection to morphisms. We provide a logical characterization of bisimilarity in the finitary case. A generalization of congruences (event bisimulations) to effectivity functions and its relation to the categorical presentation of bisimulation are also studied.

In Universal Algebra the structure of congruences for algebraic systems is fairly well investigated, and the relationship to the structure of the underlying system proper is well known. We propose a first step into this direction for studying the structure of congruences for stochastic relations. A Galois connection to a certain class of Boolean σ-algebras is exploited, atoms and antiatoms are identified, and it is show that a σ-basis exists. These constructions are applied to the problem of finding bisimulation cuts of a congruence. It cuts the relation through a span of morphisms with a minimum of joint events.

Abstract We propose a probabilistic interpretation of Propositional Dynamic Logic (PDL). We show that logical and behavioral equivalence are equivalent over general measurable spaces. This is done first for the fragment of straight line programs and then extended to cater for the nondeterministic nature of choice and iteration, expanded to PDL as a whole. Bisimilarity is also discussed and shown to be equivalent to logical and behavioral equivalence, provided the base spaces are Polish spaces. We adapt techniques from coalgebraic stochastic logic and point out some connections to Souslin's operation from descriptive set theory. This leads to a discussion of complete stochastic Kripke models and model completion, which permits an adequate treatment of the test operator.

The Coalgebraic Logic seminar took place between the 6th and 9th of December 2009 at the Leibniz Forschungszentrum Schloss Dagstuhl. The event was very well received, with more than 35 scientists from Europe, the United States, Canada and China attending, and with more than thirty presentations during the three days. Given the unforeseen enthusiasm of the meeting's reception, we thought that it would be a good idea for us to put together a special journal issue dedicated to this topic. We were also encouraged by the positive response we received from Guiseppe Longo, who indicated his interest in a special issue for Mathematical Structures in Computer Science, and here we are.

In this survey we discuss the generalisation of stochastic Kripke models for general modal logics through predicate liftings for functors over general measurable spaces. We derive results on expressivity and show that selection arguments allow us to incorporate the discussion of bisimilarity, provided the underlying spaces are assumed to be standard Borel.

We study the existence of bisimulations for Kleisli morphisms associated with the Giry monad of subprobabilities over Polish spaces. We first investigate these morphisms and show that the problem can be reduced to the existence of bisimulations for objects in the base category of stochastic relations using simulation equivalent congruences. This leads us to a criterion for two objects to be bisimilar.

The existence of semi-pullbacks for stochastic relations over analytic spaces is addressed. It is shown by means of a measure extension that the theory of measurable selectors for measurable relations may be employed for its solution. The category of stochastic relations is shown not to have (weak) pullbacks.

The relationship between congruences and bisimulations is investigated for stochastic relations. It is shown that stochastic relations are bisimilar provided they have congruences that generate each other; from this is derived that relations that have isomorphic factor spaces are bisimilar. Stochastic Kripke models are introduced for a modal logic and illustrated for some popular logics. The criterion developed here permits proving for the general case that Kripke models are bisimilar iff they accept exactly the same formulas.

Entity-Relationship modelling is a visual, hence a rather intuitive technique for specifying the structure of complex data. The technique is popular in part because the structure of an ER-model is easily grasped, and it is usually supported by diagrams or other visualizing tools. This paper deals with a detailed analysis of ER-modelling with the goal of deriving an algebraic specification for a given ER-model. This is motivated by considerations regarding program specification for data intensive applications. We indicate how the technique demonstrated here may be combined with formal techniques for specifying the functional behavior of a system.

The prototyping language ProSET (Prototyping with Sets) for experimental and evolutionary prototyping is discussed, with emphasis on algorithm design. Its features include generative communication, flexible exception handling, and the integration of persistence. Issues pertaining to the compiler and the programming environment are discussed.>

A brief discussion is presented of software prototyping. The author argues that prototypes may serve as reusable components due to the high-level nature of a prototype which eases the understanding and retrieving of programs. This general approach is illustrated by a discussion addressing the set-oriented languages SETL and Tangram/sub L/.>

The topological structure underlying the ideal model of recursive polymorphic types proposed by MacQueen, Plotkin, and Sethi are examined. It is shown that their central argument in establishing a well-defined semantical function, viz., completeness with respect to a metric obtained from the construction of their domain, is a special case of complete uniformities, which arise in a natural way from the study of closeness of ideals on domains. These uniformities are constructed and studied, and a general fixed-point theorem is derived for maps defined on these ideals.

In this note some aspects of the average behavior of the well known sorting algorithm heapsort are investigated. There are two different methods to construct heaps, which are due to Williams, and to Floyd, and for both methods the respective distribution of the heaps is computed in a continuous model. For Floyd's method moreover the expected number of interchanges, and comparisons which are necessary to construct a heap are derived. For the selection phases of both algorithms the respective distributions are investigated.