# Over-Approximation of Fluid Models

## TL;DR

This paper introduces a novel, efficient method for computing formal bounds on the reachable states of uncertain nonlinear fluid models, aiding in verification of biochemical and performance systems.

## Contribution

It relates nonlinear fluid model reachability to Markov decision processes and offers optimal control-based solutions for tight over-approximations.

## Key findings

- The method provides tight bounds on the reachable set.
- It outperforms existing over-approximation approaches.
- The technique is efficient for large-scale systems.

## Abstract

Fluid models are a popular formalism in the quantitative modeling of biochemical systems and analytical performance models. The main idea is to approximate a large-scale Markov chain by a compact set of ordinary differential equations (ODEs). Even though it is often crucial for a fluid model under study to satisfy some given properties, a formal verification is usually challenging. This is because parameters are often not known precisely due to finite-precision measurements and stochastic noise. In this paper, we present a novel technique that allows one to efficiently compute formal bounds on the reachable set of time-varying nonlinear ODE systems that are subject to uncertainty. To this end, we a) relate the reachable set of a nonlinear fluid model to a family of inhomogeneous continuous time Markov decision processes and b) provide optimal and suboptimal solutions for the family by relying on optimal control theory. The proposed technique is efficient and can be expected to provide tight bounds. We demonstrate its potential by comparing it with a state-of-the-art over-approximation approach.