ETAPS 2019 (series) / QAPL 2019 (series) / 16th Workshop on Quantitative Aspects of Programming Languages and Systems /
Automatic Synthesis of Polynomial Probabilistic Invariants via Geometric Persistence
Sun 7 Apr 2019 11:30 - 12:00 at S7 - Session II
In this paper we present an algorithm for the automatic synthesis of polynomial invariants for probabilistic transition systems. Our approach is based on martingale theory. We construct invariants in the form of polynomials over program variables, which give rise to martingales. These polynomials are program invariants in the sense that their expected value upon termination is the same as their value at the start of the computation. By exploiting geometric persistence properties of the system, we show that suitable polynomials can be automatically inferred using sum-of-squares optimisation techniques.
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 7 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | |||
11:00 30mTalk | A Faster-Than Relation for Semi-Markov Decision Processes QAPL Mathias Ruggaard Pedersen Aalborg University, Giorgio Bacci Aalborg University, Kim Larsen Aalborg University Pre-print | ||
11:30 30mTalk | Automatic Synthesis of Polynomial Probabilistic Invariants via Geometric Persistence QAPL Pre-print | ||
12:00 30mTalk | Towards Digital Twins for the Description of Automotive Software Systems QAPL Jan Olaf Blech Aalto University Pre-print |