Table of Contents
Fetching ...

Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments

Andrey Kofnov, Marcel Moosbrugger, Miroslav Stankovič, Ezio Bartocci, Efstathia Bura

TL;DR

Two methods are presented to automatically compute moment-based invariants for probabilistic programs with nonlinear non-polynomial updates in non-nested loops as closed-form solutions parameterized by the loop iteration.

Abstract

Many stochastic continuous-state dynamical systems can be modeled as probabilistic programs with nonlinear non-polynomial updates in non-nested loops. We present two methods, one approximate and one exact, to automatically compute, without sampling, moment-based invariants for such probabilistic programs as closed-form solutions parameterized by the loop iteration. The exact method applies to probabilistic programs with trigonometric and exponential updates and is embedded in the Polar tool. The approximate method for moment computation applies to any nonlinear random function as it exploits the theory of polynomial chaos expansion to approximate non-polynomial updates as the sum of orthogonal polynomials. This translates the dynamical system to a non-nested loop with polynomial updates, and thus renders it conformable with the Polar tool that computes the moments of any order of the state variables. We evaluate our methods on an extensive number of examples ranging from modeling monetary policy to several physical motion systems in uncertain environments. The experimental results demonstrate the advantages of our approach with respect to the current state-of-the-art.

Exact and Approximate Moment Derivation for Probabilistic Loops With Non-Polynomial Assignments

TL;DR

Two methods are presented to automatically compute moment-based invariants for probabilistic programs with nonlinear non-polynomial updates in non-nested loops as closed-form solutions parameterized by the loop iteration.

Abstract

Many stochastic continuous-state dynamical systems can be modeled as probabilistic programs with nonlinear non-polynomial updates in non-nested loops. We present two methods, one approximate and one exact, to automatically compute, without sampling, moment-based invariants for such probabilistic programs as closed-form solutions parameterized by the loop iteration. The exact method applies to probabilistic programs with trigonometric and exponential updates and is embedded in the Polar tool. The approximate method for moment computation applies to any nonlinear random function as it exploits the theory of polynomial chaos expansion to approximate non-polynomial updates as the sum of orthogonal polynomials. This translates the dynamical system to a non-nested loop with polynomial updates, and thus renders it conformable with the Polar tool that computes the moments of any order of the state variables. We evaluate our methods on an extensive number of examples ranging from modeling monetary policy to several physical motion systems in uncertain environments. The experimental results demonstrate the advantages of our approach with respect to the current state-of-the-art.
Paper Structure (27 sections, 3 theorems, 34 equations, 6 figures, 3 tables)

This paper contains 27 sections, 3 theorems, 34 equations, 6 figures, 3 tables.

Key Result

proposition 1

If ${\mathbf Z}=(Z_{1},\ldots, Z_{k_1})$, ${\mathbf Y}=(Y_{1},\ldots, Y_{k_2})$ satisfy conditions (A), (C) and (E) and are mutually independent, and functions $g$ and $h$ satisfy conditions (B) and (D), then their sum, $g({\mathbf Z}) + h({\mathbf Y})$, and product, $g({\mathbf Z}) \cdot h({\mathbf

Figures (6)

  • Figure 1: The probabilistic loop in the top left panel encodes the Taylor rule Taylor1993, an equation that prescribes a value for the short-term interest rate based on a target inflation rate and the gross domestic product. The program uses a non-polynomial function (log) in the loop body to update the continuous-state variable ($i$). The top right panel contains the Prob-Solvable loop (with polynomial updates) obtained by approximating the log function using polynomial chaos expansion (up to $5$th degree). In the bottom left, we compute the expected interest rate ($\mathbb{E}[i_n]$) as a closed-form expression in loop iteration $n$ using the Prob-solvable loop and evaluate it at $n=20$. In the bottom right panel, we compare the true and estimated distributions for a fixed iteration (we sample the loop $10^6$ times at iteration $n=20$).
  • Figure 2: On the left is a probabilistic loop modeling the behavior of a turning vehicle Srirametal2020 using non-polynomial (cos, sin) updates in the loop body. On the top right is the exact expected position $(x_n,y_n)$ and other exact expected values computed automatically in closed-form in the number of loop iterations $n$. The plot in the center contains $20$ sampled trajectories $(x_n,y_n)$ up to iteration $n=201$ (dashdot lines with different colors) and the approximated expected trajectory computed by averaging the sampled ones (dashed blue line). Moreover, we automatically computed the exact expected trajectory and standard deviation with our method. The solid purple line marks the exact expected trajectory. The two solid red lines mark the boundary of the region contained within $\pm$ two standard deviations of the expected trajectory.
  • Figure 3: Illustration of PCE algorithm
  • Figure 4: Probabilistic loops: (A) Rimless wheel walker SteinhardtT12 and (B) 2D Robotic arm Bouissouetal2016 (in the figure we use the inner loop as syntax sugar to keep the program compact).
  • Figure 5: Probabilistic loops: (A) Uncertain underwater vehicle Pairetetal_2020Jasouretal2021, (B) Planar aerial vehicle SteinhardtT12Jasouretal2021, (C) 3D aerial vehicle Pairetetal_2020Jasouretal2021, (D) Differential-drive mobile robot vandenBergetal_2011Jasouretal2021, (E) Stochastic decay, (F) 3D (Mobile) Robotic arm Jasouretal2014Jasouretal2021
  • ...and 1 more figures

Theorems & Definitions (7)

  • definition 1: Prob-solvable loops Bartoccietal2019
  • proposition 1
  • theorem 1
  • Remark
  • definition 2
  • lemma 1
  • definition 3: Accumulator