Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods

TL;DR

This paper presents a polynomial-time algorithm for local computation of differential bisimulations using polynomial couplings and up-to techniques, enabling efficient system reduction and comparison in dynamical systems.

Contribution

It introduces polynomial couplings and an algorithm that improves local exploration and efficiency in computing differential bisimulations, with enhancements via up-to methods.

Findings

Four orders of magnitude faster than classical methods in case studies.

Enables local exploration without full system inspection.

Applicable to model reduction and comparison in systems biology.

Abstract

We introduce polynomial couplings, a generalization of probabilistic couplings, to develop an algorithm for the computation of equivalence relations which can be interpreted as a lifting of probabilistic bisimulation to polynomial differential equations, a ubiquitous model of dynamical systems across science and engineering. The algorithm enjoys polynomial time complexity and complements classical partition-refinement approaches because: (a) it implements a local exploration of the system, possibly yielding equivalences that do not necessarily involve the inspection of the whole system of differential equations; (b) it can be enhanced by up-to techniques; and (c) it allows the specification of pairs which ought not to be included in the output. Using a prototype, these advantages are demonstrated on case studies from systems biology for applications to model reduction and comparison. Notably, we report four orders of magnitude smaller runtimes than partition-refinement approaches when disproving equivalences between Markov chains.