TU Dortmund Fakultät für Informatik

# Markov Transition Systems

Ernst-Erich Doberkat

Monographs

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

E.-E. Doberkat: Stochastic Coalgebraic Logic. Springer-Verlag, EATCS Monographs in Theoretical Computer Science, 2009

Recent Papers

1. E.-E. Doberkat: A Stochastic Interpretation of Parikh's Game Logic. April 2012, Technical Report (pdf). Parikh's game logic is a dynamic modal logic which models strategic two person games; it contains propositional dynamic logic (PDL) as a fragment. We propose a stochastic interpretation for the distributive variant of this logic based on stochastic Kripke models. The important operator which sets this logic apart from PDL is demonization, which receives due attention. The relationship of logical and behavioral equivalence of Kripke models is investigated.
2. E.-E. Doberkat: Towards a Coalgebraic Interpretation of Propositional Dynamic Logic. June 2011, Technical Report (pdf). The interpretation of propositional dynamic logic (PDL) through Kripke models requires the relations constituting the interpreting Kripke model to closely observe the syntax of the modal operators. This poses a significant challenge for an interpretation of PDL through stochastic Kripke models, because the programs' operations do not always have a natural counterpart in the set of stochastic relations. We use rewrite rules for building up an interpretation of PDL. It is shown that each program corresponds to an essentially unique irreducible tree, which in turn is assigned a predicate lifting, serving as the program's interpretation. The paper establishes and studies this interpretation. It discusses the expressivity of probabilistic models for PDL and relates properties like logical and behavioral equivalence or bisimilarity to the corresponding properties of a Kripke model for a closely related non-dynamic logic of the Hennessy-Milner type.
3. E.-E. Doberkat: A Note on the Coalgebraic Interpretation of Game Logic. Rend. Ist. Mat. Univ. Trieste 42, 2010, 191 - 205 (pdf). We propose a coalgebraic interpretation of game logic, making the methods of coalgebraic logic available for this context. We study some properties of a coalgebraic interpretation, showing among others that Aczel's Theorem on the characterization of bisimilar models through spans of morphisms is valid here. We investigate also congruences as those equivalences on the state space which preserve the structure of the model.
4. E.-E. Doberkat: A Stochastic Interpretation of Propositional Dynamic Logic: Expressivity. July 2010, Proc. 4th Indian Conf. Logic Appl., Delhi, 2011, LNCS; J. Symb. Logic 77, 2, 2012, 687 - 716 (pdf). We propose a probabilistic interpretation of Propositional Dynamic Logic (PDL). We show that logical and behavioral equivalence are equivalent over general measurable spaces. 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 $\mathcal{A}$ from descriptive set theory.
5. E.-E. Doberkat, S. M. Srivastava: Measurable Selections, Transition Probabilities and Kripke Models. May 2010, Technical Report (pdf). In this paper, we use measurable selection theorems to prove several results of independent interest on transition probabilities. As a corollary to our results we show that logical equivalence, bisimilarity and behavioral equivalence are equivalent for stochastic Kripke models over Polish spaces. This extends the classical Hennessy-Milner Theorem in modal logics to stochastic Kripke models.
6. E.-E. Doberkat, Ch. Schubert: Coalgebraic Logic Over General Measurable Spaces -- A Survey. Math. Struct. Comp. Sci. 21 (2), 2011, 175 - 234 (pdf). We discuss in this survey the generalization of stochastic Kripke models for general modal logics through predicate liftings for functors over general measurable spaces. Results on expressivity are derived, and it is shown that selection arguments permit incorporating the discussion of bisimilarity, provided the underlying spaces are assumed to be Polish.
7. E.-E. Doberkat: Quotients for the Kleisli Category over the Giry Monad. February 2010, Technical Report (pdf). Two epimorphisms $f, g$ with the same domain in a category are considered equivalent iff $f = \theta\circ g$ for some invertible $\theta$; the equivalence classes are the quotient objects. For categories in which morphisms are maps this notion of quotients coincides with the usual one, and a representative of a class is obtained through factoring. We completely characterize quotient objects for the Kleisli category over the Giry monad over Polish spaces, the morphisms of which are also known as stochastic relations. Factoring does not yield an adequate characterization, the isomorphisms for the spaces underlying the monad provide the needed identification.
8. E.-E. Doberkat: Bisimulations For Structuring Markov Transition Systems. May 2012, Technical Report (pdf). Bisimilarity is a key concept in the investigation of concurrent systems; it can be investigated coalgebraically, opening the road for the coalgebraic treatment of stochastic systems, which otherwise would be difficult to undertake. Markov transition systems model probabilistic systems in which the transition among states is represented by probabilistic laws. Stochastic relations lie at the mathematical heart of Markov transition systems. We show in this paper that a stochastic relation can be decomposed along a given congruence so that the parts are bisimilar (with the original relation as a mediating component); this result is the bisimulation analogue to the classical decomposition of algebras through complementary congruences. We apply this technique also to Kripke models for modal logics.
9. 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.
10. E.-E. Doberkat: Lattice Properties of Congruences for Stochastic Relations. March 2009, Ann. Pure Appl. Logic 163 (2012) 1016 - 1029 (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.
11. 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.
12. 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.
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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.
19. 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.
20. 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.
21. 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).
22. 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.
23. 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.
24. 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.
25. 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.
26. 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.
27. 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.
28. 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.
29. 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.
30. 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.

© Technische Universität Dortmund, Fakultät für Informatik, Lehrstuhl für Software-Technologie
Content-Management-System Typo3