Computing continuous-time Markov chains as transformers of unbounded observables

Abstract

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.