Publications

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

Andrey Kofnov Marcel Moosbrugger Miroslav Stankovič Ezio Bartocci Efstathia Bura

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.

ACM Trans. on Modeling and Comp. Simul. 2024 22 January 2024

Strong Invariants Are Hard - On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs

Julian Müllner Marcel Moosbrugger Laura Kovács

We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem.

POPL 2024 15 January 2024

Automated Sensitivity Analysis for Probabilistic Loops

Marcel Moosbrugger Julian MÜllner Laura Kovács

We present an exact approach to analyze and quantify the sensitivity of higher moments of probabilistic loops with symbolic parameters, polynomial arithmetic and potentially uncountable state spaces.

IFM 2023 15 November 2023

Deductive Controller Synthesis for Probabilistic Hyperproperties

Roman Andriuschenko Ezio Bartocci Milan Češka Francesco Pontiggia Sarah Sallinger

We present a deductive algorithm for the POMDP controller synthesis problem against probabilistic hyperproperties specifications.

QEST 2023 25 September 2023

From Polynomial Invariants to Linear Loops

George Kenison Anton Varonka Laura Kovacs

We prove the existence of non-trivial loops with linear updates for polynomial invariants generated by pure difference binomials.

ISSAC 2023 21 May 2023

The Membership Problem for Hypergeometric Sequences with Quadratic Parameters

George Kenison Klara Nosan Mahsa Shirmohammadi James Worrell

We establish decidability results for the Membership Problem for certain classes of hypergeometric sequences.

ISSAC 2023 21 May 2023

Positivity Problems for Reversible Linear Recurrence Sequences

George Kenison Joris Nieuwveld Joël Ouaknine James Worrell

We consider variants of the Positivity Problem for linear recurrence sequences.

ICALP 2023 21 May 2023

The probabilistic termination tool amber

Marcel Moosbrugger Ezio Bartocci Joost-Pieter Katoen Laura Kovács

We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner.

Formal Methods in System Design 2023 10 May 2023

This is the Moment for Probabilistic Loops

Marcel Moosbrugger Miroslav Stankovic Ezio Bartocci Laura Kovacs

We present a novel static analysis technique to derive higher moments for program variables for a large class of probabilistic loops with potentially uncountable state spaces.

OOPSLA 2022 01 September 2022

Solving Invariant Generation for Unsolvable Loops

Daneshvar Amrollahi Ezio Bartocci George Kenison Laura Kovacs Marcel Moosbrugger Miroslav Stankovic

In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops.

SAS 2022 16 July 2022

Distribution Estimation for Probabilistic Loops

Ahmad Karimi Miroslav Stankovič Marcel Moosbrugger Laura Kovács Ezio Bartocci Efstathia Bura

We present an algorithmic approach to estimate the value distributions of random variables of probabilistic loops whose statistical moments are (partially) known.

QEST 2022 21 June 2022

Moment-based Invariants for Probabilistic Loops with non-polynomial assignments

Andrey Kofnov Marcel Moosbrugger Miroslav Stankovic Ezio Bartocci Efstathia Bura

We present a method to automatically approximate moment-based invariants of probabilistic programs with non-polynomial updates of continuous state variables to accommodate more complex dynamics.

QEST 2022 21 June 2022

On the Skolem Problem for Reversible Sequences

George Kenison

This paper presents an alternative proof of a recent breakthrough for the Reversible Skolem Problem.

MFCS 2022 21 June 2022

Probabilistic Hyperproperties with Rewards

Lukas Wilke Oyendrila Dobe Erika Abraham Ezio Bartocci Borzoo Bonakdarpour

This paper introduces the notion of rewards to the temporal logic HyperPCTL by extending the syntax and semantics of the logic to express the accumulated reward relation among different computations.

NASA Formal Methods 2022 01 April 2022

Algebra-Based Reasoning for Loop Synthesis

Andreas Humenberger Daneshvar Amrollahi Nikolaj Bjørner Laura Kovács

This paper presents an algorithm for synthesizing loops satisfying a given polynomial loop invariant.

Formal Aspects of Computing 01 March 2022

Moment-Based Analysis of Bayesian Network Properties

Miroslav Stankovic Ezio Bartocci Laura Kovacs

We use algebraic reasoning to translate Bayesian network (BN) properties into linear recurrence equations over statistical moments of BN variables. This paper is an extended version of our ICTAC 2020 paper.

Journal of Theoretical Computer Science 28 December 2021

The Probabilistic Termination Tool Amber

Marcel Moosbrugger Ezio Bartocci Joost-Pieter Katoen Laura Kovács

We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner.

FM 2021 26 November 2021

On Positivity and Minimality for Second-Order Holomonic Sequences

George Kenison Oleksiy Klurman Engel Lefaucheux Florian Luca Pieter Moree Joël Ouaknine Markus Whiteland James Worrell

In this paper we give a Turing reduction of the problem of deciding positivity of second-order holonomic sequences to that of deciding minimality of such sequences.

MFCS 2021 23 August 2021

Automated Termination Analysis of Polynomial Probabilistic Programs

Marcel Moosbrugger Ezio Bartocci Joost-Pieter Katoen Laura Kovács

This paper presents a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions.

ESOP 2021 27 March 2021

Analysis of Bayesian Networks via Prob-Solvable Loops

Ezio Bartocci Miroslav Stankovic Laura Kovács

We show that various BNs, such as discrete, Gaussian, conditional linear Gaussian and dynamic BNs, can be naturally encoded as Prob-solvable loops. Thanks to these encodings, we can automatically solve several BN related problems, including exact inference, sensitivity analysis, filtering and computing the expected number of rejecting samples in sampling-based procedures.

ICTAC 2020 20 September 2020

Probabilistic Hyperproperties with Nondeterminism

Erika Ábrahám Ezio Bartocci Borzoo Bonakdarpour Oyendrila Dobe

We study the problem of formalizing and checking probabilistic hyperproperties for Markov Decision Processes.

ATVA 2020 01 June 2020

Mora - Automatic Generation of Moment-Based Invariants

Ezio Bartocci Miroslav Stankovic Laura Kovács

We introduce Mora, an automated tool for generating invariants of probabilistic programs. Inputs to Mora are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions.

TACAS 2020 02 January 2020

Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops

Ezio Bartocci Miroslav Stankovic Laura Kovács

We present a method to automatically generate moment-based invariants of a subclass of probabilistic programs, called Prob-Solvable loops, with polynomial assignments over random variables and parametrised distributions.

ATVA 2019 01 June 2019