Stochastic transition systems: bisimulation, logic, and composition

Cyber-physical systems and the Internet of Things raise various challenges concerning the modelling and analysis of large modular systems. Models for such systems typically require uncountable state and action spaces, samplings from continuous distributions, and non-deterministic choices over uncountable many alternatives. In this thesis we fo- cus on a general modelling formalism for stochastic systems called stochastic transition system. We introduce a novel composition operator for stochastic transition systems that is based on couplings of probability measures. Couplings yield a declarative modelling paradigm appropriate for the formalisation of stochastic dependencies that are caused by the interaction of components. Congruence results for our operator with respect to standard notions for simulation and bisimulation are presented for which the challenge is to prove the existence of appropriate couplings. In this context a theory for stochastic transition systems concerning simulation, bisimulation, and trace-distribution relations is developed. We show that under generic Souslin conditions, the simulation preorder is a subset of trace-distribution inclusion and accordingly, bisimulation equivalence is finer than trace-distribution equivalence. We moreover establish characterisations of the simulation preorder and the bisimulation equivalence for a broad subclass of stochastic transition systems in terms of expressive action-based probabilistic logics and show that these characterisations are still maintained by small fragments of these logics, respectively. To treat associated measurability aspects, we rely on methods from descriptive set theory, properties of Souslin sets, as well as prominent measurable-selection principles.:1 Introduction 2 Probability measures on Polish spaces 3 Stochastic transition systems 4 Simulations and trace distributions for Souslin systems 5 Action-based probabilistic temporal logics 6 Parallel composition based on spans and couplings 7 Relations to models from the literature 8 Conclusions 9 Bibliograph