Markov Transition Systems

Ernst-Erich Doberkat

Monographs

E.-E. Doberkat: Stochastic Relations. Foundations for Markov Transition Systems. Chapman & Hall, New York, 2007 (Typos).  

E.-E. Doberkat: Stochastic Coalgebraic Logic. Springer-Verlag, 2009, in print

Recent Papers

1. E.-E. Doberkat: Negating Congruences for Stochastic Relations. October 2009, Technical Report (pdf). Given an equivalence relation $\rho$, we investigate modelling the negation of $\rho$ through an equivalence relation $\rho'$ so that $\rho\wedge\rho'$ is the identity and $\rho$ together with $\rho'$ is comprehensive, i.e., $\rho\vee\rho'$ covers the entire space. This looks very much like complementation, but the lattice of equivalence relations is complemented only in very rare special cases, in particular under the constraints which are imposed in the present paper. We are interested in congruences for stochastic relations, so we investigate from the starting point above under which conditions a congruence can be negated, ending up with a variety of constructions that all are more or less intended to characterize non-congruent objects. This is applied to morphisms, a simple version von Hennessy-Milner logic serves as an illustration.
2. E.-E. Doberkat: Tutorial Stochastic Coalgebraic Logic, ISDT'09, Shanghai, September 2009. (Slides) A brief and tutorial overview of the development of coalgebraic logics from modal logics, looking through the glasses of stochastic Kripke models and the associated coalgebraic approaches.
3. E.-E. Doberkat: Lattice Properties of Congruences for Stochastic Relations. March 2009, Technical Report (pdf). We have a look at the set of congruences for a stochastic relation; conditions under which the infimum or the supremum of two congruences is a congruence again are investigated. Congruences are based on smooth equivalence relations, and consequences of the observation that the supremum of two smooth relations may fail to be smooth are discussed: analytic spaces are not closed under pushouts, and the set of countably generated $\sigma$-algebras is not closed under finite intersections.
4. E.-E. Doberkat: Behavioral and Logical Equivalence of Stochastic Kripke Models in General Measurable Spaces. Proc. Theor. Appl. Mod. Comput. TAMC'2009 Changsha, LNCS 5532, pp. 192 -- 200, 2009. (pdf) We show that logical and behavioral equivalence for stochastic Kripke models over general measurable spaces are the same. Usually, this requires some topological assumptions and includes bisimilarity; the results here indicate that a measurable structure on the state space of the Kripke model suffices. In contrast to a paper by Danos et al. we focus on the measurable structure of the factor space induced by the logic. This technique worked well in the analytic case, and it is shown to work here as well. The main contribution of the paper is methodological, since it provides a uniform framework for general measurable as well as more specialized analytic spaces.
5. E.-E. Doberkat: Weak Bisimulations for the Giry Monad. December 2007. Proc. Theor. Appl. Mod. Comput. TAMC'2008 Xi'an, LNCS 4978, 400--409, special issue, Math. Struct. Comp. Sci. (pdf). The existence of bisimulations for objects in the Kleisli category associated with the Giry monad of subprobabilities over Polish spaces is studied. 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 to a criterion for two objects related through the monad to be bisimilar. 
6. E.-E. Doberkat, C. Schubert: Coalgebraic logic for stochastic right coalgebras. J. Pure Appl. Logic, 159, 2009, 268 - 284 (pdf). We generalize stochastic Kripke models and Markov transition systems to stochastic right coalgebras. These are coalgebras for a functor F o S with F as an endofunctor on the category of analytic spaces, and S is the subprobability functor. The modal operators are generalized through predicate liftings which are set-valued natural transformations involving the functor. Two states are equivalent iff they cannot be separated by a formula. This equivalence relation is used to construct a cospan for logical equivalent coalgebras under a separation condition for the set of predicate liftings. Consequently, behavioral and logical equivalence are really the same. From the cospan we construct a span. The central argument is a selection argument giving us the dynamics of a mediating coalgebra from the domains of the cospan. This construction is used to establish that behavioral equivalent coalgebras are bisimilar, yielding the equivalence of all three characterizations of a coalgebra's behavior as in the case of Kripke models or Markov transition systems.
7. E.-E. Doberkat: Bisimilarity of Distributionally Equivalent Markov Transition Systems. Proc. FICS'08 Shanghai; ENTCS  212, 2008, 41 - 53 (pdf). Markov transition systems for interpreting a modal logic are called distributionally equivalent iff  for each formula the probability for its extension in one model is matched probabilistically in the other one. This extends  in a natural way the notion of logical equivalence which is defined on the states of a transition system to its subprobability distributions. It is known that logical equivalence is equivalent to  bisimilarity, i.e., the existence of a span of Borel maps that act as morphisms. We show that distributional equivalence is equivalent to bisimilarity as well, using a characterization of distributional equivalent transition systems through ergodic morphisms. We also relate bisimilar transition systems to strongly or weakly behavioral equivalent systems, i.e., systems for which cospans --- taken in the category of measurable maps resp. in the Kleisli category associated with the Giry monad --- exist.  
8. E.-E. Doberkat: Stochastic Coalgebraic Logic: Bisimilarity and Behavioral Equivalence.  Ann. Pure Appl. Logic, 155, 2008, 46 - 68 (pdf). Bisimulations, behavioral equivalence and logical equivalence are investigated for stochastic T coalgebras that interpret coalgebraic logic which is defined in terms of predicate liftings. It is investigated under which conditions for the functor these notions of equivalence are related by discussing congruences for the underlying stochastic relation. It is demonstrated that logics so diverse as continuous time stochastic logic and general modal logics can be usefully approached through coalgebraic methods.
9. E.-E. Doberkat: Kleisli Morphisms and Randomized Congruences for the Giry Monad. April 2006. J. Pure and Appl. Algebra, 211, 2007, 638-664 (pdf). Stochastic relations are the Kleisli morphisms for the Giry monad. This paper proposes the study of the associated morphisms and congruences. The relationship between kernels of these morphisms and congruences is studied, and  a unique factorization of a morphism  through this kernel is shown to exist. This study is based on an investigation into countably generated equivalence relations on the space of all subprobabilities. Operations these relations are investigated quite closely. This utilizes positive convex structures and indicates cross connections to Eilenberg-Moore algebras for the Giry monad. Hennessy-Milner logic serves as an illustration for randomized morphisms and congruences.
10. E.-E. Doberkat: Hyperfinite Approximations to Labeled Markov Transition Systems. M. Johnson, V. Vene (Eds.): Proc. AMAST 2006, 127 -- 141, LNCS 4019 (bib, pdf). The problem of finding an  approximation to a labeled Markov transition system through hyperfinite transition systems is addressed. It is shown that we can find for each countable family of stochastic relations on Polish spaces a family of relations defined on a hyperfinite set that is infinitely close. This is applied to Kripke models for a simple modal logic in the tradition of Larsen and Skou. It follows that we can find for each Kripke model a hyperfinite one which is infinitely close.
11. E.-E. Doberkat: Eilenberg-Moore algebras for stochastic relations. Information and Computation 204, 2006, 1756 - 1781 (zip, Erratum). The Eilenberg-Moore algebras for the Giry monad of all subprobability measures on Polish spaces with continuous maps as morphisms are investigated. They are identified as the positive convex structures on a base space and vice versa: each positive convex structure corresponds uniquely to an algebra, generalizing a well known result for the probability functor from compact Hausdorff spaces to Polish spaces. The forgetful functor assigning a positive convex structure its underlying Polish spaces has the stochastic powerdomain as its left adjoint.
12. E.-E. Doberkat: The Hennessy-Milner equivalence for continuous time stochastic logic with mu-operator. J. Appl. Logic, 5, 2007, 519 - 544 (bib, zip). A continuous stochastic logic with a $\mu$-operator called $\muCSL$ is defined, and an interpretation through stochastic relations is proposed. We investigate morphisms for models of $\muCSL$, showing that the associated congruences can be used for an investigation of bisimilarity. The Hennessy-Milner equivalence for $\muCSL$ is discussed, and it is shown that models are equivalent iff they are bisimilar, using a general criterion for bisimilarity from the theory of stochastic relations.
13. E.-E. Doberkat: Stochastic relations: congruences, bisimulations and the Hennessy-Milner Theorem. SIAM J. Computing 35, 2006, 590 - 626 (bib, zip) Congruences are investigated more closely. In [4] it was shown that two stochastic relations are bisimilar iff they accept the same formulas of a very simple modal logic. This leads directly to the notion of a congruence (as in [6]) and to the question of characterizing bisimilarity intrinsically, hence without having to refer to an external instance like a logic. It is shown that such a criterion can be found through equivalent congruences. As a consequence it is established that stochastic relations which have isomorphic subsystems are bisimilar. This is true in any analytic space, and it is shown that the converse holds under a compactness assumption. We make the conjecture that having isomorphic subsystems and bisimilarity are equivalent for stochastic relations. General modal logics can be interpreted through stochastic Kripke structures, i.e. Kripke structures based on stochastic relations, generalizing the approach due to Desharnais, Edalat and Panangaden, and from [4], moreover it is shown that bisimilarity and accepting the same formulas are equivalent conditions (the Hennessy-Milner Theorem) in general analytic spaces without the smallness assumption from [4] or the assumption of universal measurability, as in the paper by Desharnais, Edalat and Panangaden.
14. E.-E. Doberkat: Semi-Pullbacks and Bisimulations in Categories of Stochastic Relations. In J. C. Baeten, J. K. Lenstra, J. Parrow, G. J. Woeginger (Ed.): Proc. 30th Inter. Coll. on Automata, Languages and Programming 2003, 996-1007,   LNCS 2719, Springer, 2003 (bib, zip) It was a long standing open problem whether or not the category of stochastic relations over Polish spaces with surjective measurable maps has semi-pullbacks. A first step at tackling the problem was done by Edalat, who showed by direct construction that the category of stochastic relations over analytic spaces with universally measurable maps as morphisms has semi-pullbacks. The ICALP-paper shows by a selection argument quite independent of Edalat’s construction established the existence also for the originally given category (which is quite natural for most constructions pertaining to stochastic relations and Markov labeled transition processes). This is applied to a very simple modal logic without negation, it is shown that two Markov labelled transition processes accept the same formulas iff they are bisimilar, provided the processes are small (this is a generalization of a result by Edalat, Panangaden and Desharnais).
15. E.-E. Doberkat: Semi-Pullbacks for Stochastic Relations over Analytic Spaces. Math. Struct. Comp. Sci. 15, 2005, 647 - 670 (bib, zip) The solution concerning the existence of semi-pullbacks is generalized from [4]: while there the basic scenario consisted of Polish spaces with measurable surjections, we discuss in this paper the much wider class of analytic spaces with these morphisms, and show that semi-pullbacks exist for stochastic relations in this category. The proof depends on a measure extension argument from a Polish space to its compactification in the Hilbert cube, and on a selection argument for weakly measurable set-valued maps. It is non-constructive since the axiom of choice is used through the Hahn-Banach Theorem. This seems to be the most general solution to this problem.
16. E.-E. Doberkat: Factoring Stochastic Relations. Information Processing Letters 90, 2004, 161-166 (bib, zip) We propose the notion of a congruence for stochastic relations as a pair of smooth equivalence relations (r, s) such that s-invariant Borel sets are assigned the same probability under r-equivalent inputs (an equivalence relation on an analytic space is called smooth iff it has a countable generator made up from Borel sets, or, equivalently, iff it is the kernel of a measurable map into a Polish space). Factoring a stochastic relation is investigated, and the arising analytic spaces are investigated: an isomorphism theorem akin to E. Noether’s Second Isomorphism Theorem in group theory is established, and it is shown through a reduction technique that iterated factoring does not yield new structures.
17. E.-E. Doberkat: Pipelines: Modelling a Software Architecture Through Relations. Acta Informatica  40, 2003, 37-79 (bib, zip) We model the work of a pipeline through a monad over a category with finite products and tensorial strength similar to Moggi’s \lambda_ calculus (sample monads include the power set monad in the category of sets and the subprobability monad in the category of measurable spaces). Technical problems include the synchronization of the components which are overcome through a stratification approach. Concatenation and substitution of subsystems are represented in this framework, leading to a construction kit for pipeline architectures.
18. E.-E. Doberkat: Look - simple stochastic relations are, well, just simple. In J. Fiadeiro, J. Rutten (Eds.): Proc. CALCO, LNCS 3629, 128 - 142, 2005 (bib, zip). A relation is simple iff it does not have any non-trivial subsystems, or, equivalently, iff each epi that has the relation as a source is an iso. We characterize simple relations in terms of bisimulations: a system is simple iff it has only trivial bisimulations. This is established for stochastic relations defined over analytic spaces. A little more can be said it the underlying spaces are Polish: then a relation is simple iff there is at most one morphism into it. As a by-product we show that each congruence on a Polish object can be extended to a bisimulation; this seems to be a non-trivial observation, its proof is based on a selection argument for set-valued maps. Using the characterization, it is shown that only the one-point relation is final in the subcategory of probabilistic relations (that assign probability 1 to the whole space), and the injective Borel maps are identified as the simple relations for the general case.
19. E.-E. Doberkat: Zeno paths, congruences and bisimulations for continuous-time stochastic logic. In Dang Van Hung and M.Wirsing, editors, Proc. ICTAC'2005,  Hanoi, LNCS 3722, 422 - 436, 2005.(bib, zip1, zip2). Continuous stochastic logic (CSL) deals with the verification of systems operating in continuous time, it may be traced to the well known logic CTL.  The present logic contains a next as well as an until operator, and it permits expressing steady-state probabilities. We establish in this paper a probabilistic interpretation of this logic which is based on stochastic relations without making specific assumptions on the underlying distribution: usually some kind of exponential distribution based on a rate function is imposed, but these assumptions are shown to be unnecessarily restrictive. We study the problem of bisimulations in this fairly general context from the viewpoint of congruences for stochastic relations. The main contribution is to provide a general context for the interpretation of the logic including the steady-state operator, and establishing some new results on bisimulations. Methodically, congruences are used to derive practical results for testing.
20. E.-E. Doberkat: Tracing Relations Probabilistically. In: R. Berghammer, B. Möller, R. Struth (Eds.): Relational and Kleene-Algebraic Methods in Computer Science, 86 -- 98,  LNCS, 3051, Springer, 2004. Full version Fund. Inform. 66, 3, 259 - 275, 2005 (bib, zip)   Given a family of nondeterministic relations, we show that this family expands to an infinite tree (which is essentially determined through all possible trajectories). It is shown that a probabilistic counterpart can also be constructed from a a family of stochastic relations (the construction is essentially given through the projective limit). Both kinds of relations behave in the same way, so the question is investigated whether a given infinite measurable tree can be constructed from stochastic relations as the set of all feasible probabilistic trajectories. The affirmative answer requires some topological assumptions, it is shown how it is constructed.
21. E.-E. Doberkat: The Converse of a Probabilistic Relation. In A. Gordon (Ed.): Proc. Foundation of Software Science and Computational Structures 2003, 233-249, LNCS 2620, Springer, 2003.  Journal of Algebraic and Logic Programming, 62, 2005, 133 - 154  (bib, zip1, zip2) Forming the converse of a nondeterministic relation is easy, but requires considerable preparations in the stochastic case: it is proposed that the converse is constructed through disintegration. The construction is investigated: a nondeterministic sidekick of a stochastic relation is identified and shown to be related through a natural transformation, it is shown that the converse forms almost everywhere a weakly compact set of measures, and finally it is established that forming the converse and bisimilarity are compatible. Most constructions require some topological assumptions, we work usually in a Polish space.
22. E.-E. Doberkat: The Demonic Product of Probabilistic Relations. In Mogens Nielsen (Ed.): Proc. Foundation of Software Science and Computational Structures 2002, 113-127, LNCS 2303, Springer, 2002 (bib, zip1, zip2) The demonic product is well known for set theoretic relations, and it is shown here how a very similar construction can be carried out for the probabilistic case. The paper proposes two notions of bisimilarity for stochastic relations, one oriented towards the relational definition given by Milner, the other one coalgebraic in the sense of Rutten. It is shown that these definitions are equivalent under rather mild topological conditions. The demonic product is shown to be maintained under bisimilarity, and it is shown that there are close ties between the nondeterministic and the stochastic concept.
23. E.-E. Doberkat and E. G. Omodeo: ER-Modeling From First Relational Principles. Theoretical Computer Science 311 (1-3), 2004, 285-323 (bib, zip) We show that a simple entity relationship model can be represented through an untyped relational algebra. Invariants for the model and rules for inserting and deleting elements are given, and it is demonstrated in detail how the Abstract Data Type ER model is maintained.