TY - GEN

T1 - Computing continuous-time Markov chains as transformers of unbounded observables

AU - Danos, Vincent

AU - Heindel, Tobias

AU - Garnier, Ilias

AU - Simonsen, Jakob Grue

N1 - Conference code: 20

PY - 2017

Y1 - 2017

N2 - The paper studies continuous-time Markov chains (CTMCs) as transformers of real-valued functions on their state space, considered as generalised predicates and called observables. Markov chains are assumed to take values in a countable state space S; observables f: S → ℝ may be unbounded. The interpretation of CTMCs as transformers of observables is via their transition function Pt: each observable f is mapped to the observable Ptf that, in turn, maps each state x to the mean value of f at time t conditioned on being in state x at time 0. The first result is computability of the time evolution of observables, i.e., maps of the form (t, f) ↦ Ptf, under conditions that imply existence of a Banach sequence space of observables on which the transition function Pt of a fixed CTMC induces a family of bounded linear operators that vary continuously in time (w.r.t. the usual topology on bounded operators). The second result is PTIME-computability of the projections t ↦ (Ptf)(x), for each state x, provided that the rate matrix of the CTMC Xt is locally algebraic on a subspace containing the observable f. The results are flexible enough to accommodate unbounded observables; explicit examples feature the token counts in stochastic Petri nets and sub-string occurrences of stochastic string rewriting systems. The results provide a functional analytic alternative to Monte Carlo simulation as test bed for mean-field approximations, moment closure, and similar techniques that are fast, but lack absolute error guarantees.

AB - The paper studies continuous-time Markov chains (CTMCs) as transformers of real-valued functions on their state space, considered as generalised predicates and called observables. Markov chains are assumed to take values in a countable state space S; observables f: S → ℝ may be unbounded. The interpretation of CTMCs as transformers of observables is via their transition function Pt: each observable f is mapped to the observable Ptf that, in turn, maps each state x to the mean value of f at time t conditioned on being in state x at time 0. The first result is computability of the time evolution of observables, i.e., maps of the form (t, f) ↦ Ptf, under conditions that imply existence of a Banach sequence space of observables on which the transition function Pt of a fixed CTMC induces a family of bounded linear operators that vary continuously in time (w.r.t. the usual topology on bounded operators). The second result is PTIME-computability of the projections t ↦ (Ptf)(x), for each state x, provided that the rate matrix of the CTMC Xt is locally algebraic on a subspace containing the observable f. The results are flexible enough to accommodate unbounded observables; explicit examples feature the token counts in stochastic Petri nets and sub-string occurrences of stochastic string rewriting systems. The results provide a functional analytic alternative to Monte Carlo simulation as test bed for mean-field approximations, moment closure, and similar techniques that are fast, but lack absolute error guarantees.

UR - http://www.scopus.com/inward/record.url?scp=85015940232&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-54458-7_20

DO - 10.1007/978-3-662-54458-7_20

M3 - Article in proceedings

AN - SCOPUS:85015940232

SN - 978-3-662-54457-0

T3 - Lecture notes in computer science

SP - 338

EP - 354

BT - Foundations of Software Science and Computation Structures

A2 - Esparza, Javier

A2 - Murawski, Andrzej S.

PB - Springer

Y2 - 22 April 2017 through 29 April 2017

ER -