Hybrid Behaviour of Markov Population Models

TL;DR

This paper studies the hybrid behavior of population models in stochastic concurrent constraint programming, proving their convergence to hybrid systems as population size increases, including models with complex transition conditions.

Contribution

It introduces a hybrid semantics for sCCP models and proves their convergence to hybrid systems, extending understanding of population model approximations.

Findings

Sequence of CTMCs converges to hybrid systems with increasing population size.

Hybrid semantics correctly approximate the limiting behavior of sCCP models.

Convergence holds even with guarded and instantaneous transitions.

Abstract

We investigate the behaviour of population models written in Stochastic Concurrent Constraint Programming (sCCP), a stochastic extension of Concurrent Constraint Programming. In particular, we focus on models from which we can define a semantics of sCCP both in terms of Continuous Time Markov Chains (CTMC) and in terms of Stochastic Hybrid Systems, in which some populations are approximated continuously, while others are kept discrete. We will prove the correctness of the hybrid semantics from the point of view of the limiting behaviour of a sequence of models for increasing population size. More specifically, we prove that, under suitable regularity conditions, the sequence of CTMC constructed from sCCP programs for increasing population size converges to the hybrid system constructed by means of the hybrid semantics. We investigate in particular what happens for sCCP models in which some transitions are guarded by boolean predicates or in the presence of instantaneous transitions.