Search Results

Probabilistic programs and stochastic models have become a central paradigm for describing systems operating under uncertainty, ranging from randomised algorithms and Bayesian inference to cyber-physical systems. Their formal analysis, however, remains highly challenging due to the interplay among probabilistic behaviour, nondeterminism, and potentially unbounded computations. In recent years, martingale-based reasoning and moment-based and recurrence-equation approaches have emerged as powerful techniques for the automated verification of probabilistic loops [Ezio Bartocci et al., 2019; Marcel Moosbrugger et al., 2022]. We present a line of work [Daneshvar Amrollahi et al., 2022; Daneshvar Amrollahi et al., 2025; Ezio Bartocci, 2024; Ezio Bartocci et al., 2019; Ezio Bartocci et al., 2020; Ezio Bartocci et al., 2020; Andrey Kofnov et al., 2022; Andrey Kofnov et al., 2024; Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2023; Marcel Moosbrugger et al., 2024; Marcel Moosbrugger et al., 2022; Miroslav Stankovic and Ezio Bartocci, 2024; Miroslav Stankovic et al., 2022] on the automated reasoning about probabilistic programs through moment-based analysis, recurrence solving, and asymptotic reasoning. A key observation is that, for the class of Prob-Solvable loops, it is always possible to characterise higher-order statistical moments via systems of linear recurrence equations admitting computable closed forms [Ezio Bartocci et al., 2019; Ezio Bartocci et al., 2020]. This feature enables the systematic derivation of quantitative properties such as expected values, variances, and probabilistic termination guarantees. We first introduce the class of probabilistic (potentially infinite) loops that we call Prob-Solvable. For every loop in this class we can compute, analytically and without sampling, the exact higher-order statistical moments as closed-form expressions of the number of iterations. Moreover, we develop a faithful encoding of several families of Bayesian networks (BNs) into Prob-Solvable loops. In particular, BNs can be represented as probabilistic loops with polynomial assignments over random variables, enabling automated reasoning about exact inference, filtering, sensitivity analysis, and sampling-based procedures through invariant generation and closed-form recurrence solving [Ezio Bartocci et al., 2020; Miroslav Stankovic et al., 2022]. The proposed framework supports discrete, Gaussian, conditional linear Gaussian, and dynamic BNs, extending probabilistic program analysis to a broad family of probabilistic graphical models. Beyond Prob-Solvable loops, we also characterise a hierarchy of solvable and unsolvable probabilistic loop classes and extend moment-based analysis to loops with non-polynomial assignments [Daneshvar Amrollahi et al., 2022; Daneshvar Amrollahi et al., 2025; Andrey Kofnov et al., 2022; Andrey Kofnov et al., 2024]. These works widen the applicability of symbolic techniques beyond the original polynomial setting. The resulting algorithms are implemented in tools such as Mora [Ezio Bartocci et al., 2020] and Polar [Marcel Moosbrugger et al., 2024]. While Mora focuses on the automatic generation of moment-based invariants only for probabilistic loops with polynomial assignments, Polar provides a more general algebraic framework for exact symbolic analysis of probabilistic loops and related stochastic models [Marcel Moosbrugger et al., 2024]. We further investigate the inverse problem of synthesising probabilistic loops from prescribed moment sequences, thereby complementing analysis with program construction techniques [Miroslav Stankovic and Ezio Bartocci, 2024]. We then turn to verifying probabilistic termination properties. In this setting, martingale-based proof rules provide sufficient conditions for establishing almost-sure termination (AST), positive almost-sure termination (PAST), as well as non-termination properties. The key challenge lies in automating these proof obligations. To overcome this, we introduce Amber, a fully automated framework for proving and refuting the probabilistic termination of polynomial loops [Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2021; Marcel Moosbrugger et al., 2023]. Amber blends martingale reasoning with asymptotic bounds obtained from recurrence equations and handles symbolic constants as well as standard probability distributions. A common thread running through these papers is the reduction of probabilistic reasoning to symbolic algebraic reasoning. By expressing expected values and higher-order moments of stochastic updates as systems of recurrence equations, automated techniques can be applied for solving recurrences, generating invariants, and performing asymptotic analysis. This combination of probability theory, formal methods, and symbolic computation yields exact or asymptotically tight properties of stochastic systems and offers a viable pathway to automate quantitative verification tasks that would otherwise be intractable.

We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automata. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs.