Cover Image

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Haase, Darion, Batz, Kevin, Gallus, Adrian, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Klinkenberg, Lutz, Winkler, Tobias
Format:	Preprint
Published:	2026
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
by: Schröer, Philipp, et al.
Published: (2025)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
by: Klinkenberg, Lutz, et al.
Published: (2023)

Caesar: A Deductive Verifier for Probabilistic Programs
by: Schröer, Philipp, et al.
Published: (2026)

Unknown Biases and Timing Constraints in Timed Automata
by: Haase, Darion, et al.
Published: (2024)

Verifying Sampling Algorithms via Distributional Invariants
by: Zilken, Daniel, et al.
Published: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
by: Batz, Kevin, et al.
Published: (2024)

Model Checking Temporal Properties of Recursive Probabilistic Programs
by: Winkler, Tobias, et al.
Published: (2021)

Quantifier Elimination and Craig Interpolation, Quantitatively
by: Batz, Kevin, et al.
Published: (2025)

Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
by: Schröer, Philipp, et al.
Published: (2026)

Markov Decision Processes with Sure Parity and Multiple Reachability Objectives
by: Berthon, Raphaël, et al.
Published: (2024)

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
by: Mertens, Hannah, et al.
Published: (2024)

Compositional Reasoning for Parametric Probabilistic Automata
by: Mertens, Hannah, et al.
Published: (2025)

Compositional Reasoning for Probabilistic Automata with Uncertainty
by: Mertens, Hannah, et al.
Published: (2026)

Programming and Reasoning in Partially Observable Probabilistic Environments
by: Gürtler, Tobias, et al.
Published: (2025)

noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning
by: Gürtler, Tobias, et al.
Published: (2026)

IC3 for Probabilistic Systems
by: Batz, Kevin
Published: (2024)

Probabilistic Model Checking Taken by Storm
by: Volk, Matthias, et al.
Published: (2026)

A Spectrum of Approximate Probabilistic Bisimulations
by: Spork, Timm, et al.
Published: (2024)

Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
by: Spork, Timm, et al.
Published: (2025)

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
by: Gerlach, Lina, et al.
Published: (2025)

The Algebra of Iterative Constructions
by: Batz, Kevin, et al.
Published: (2026)

A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
by: Berthon, Raphaël, et al.
Published: (2025)

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation
by: Yang, Xiaoxiao, et al.
Published: (2017)

Towards Concurrent Quantitative Separation Logic
by: Fesefeldt, Ira, et al.
Published: (2022)

Bayesian Inference in Quantum Programs
by: Gehnen, Christina, et al.
Published: (2025)

First-Order LTLf Synthesis with Lookback (Extended Version)
by: Winkler, Sarah
Published: (2025)

Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata
by: Geißler, Dominik, et al.
Published: (2025)

Artifact for Paper: Multi-Cost-Bounded Reachability Analysis of POMDPs
by: Bork, Alexander, et al.
Published: (2025)

Verification of Robust Multi-Agent Systems
by: Berthon, Raphaël, et al.
Published: (2026)

Natural Strategic Ability in Stochastic Multi-Agent Systems
by: Berthon, Raphaël, et al.
Published: (2024)

Probabilistic Byzantine Fault Tolerance (Extended Version)
by: Avelãs, Diogo, et al.
Published: (2024)

Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
by: Ahrens, Emma, et al.
Published: (2025)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
by: Verscht, Lena, et al.
Published: (2024)

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
by: Heck, Linus, et al.
Published: (2025)

Weighted Automata for Exact Inference in Discrete Probabilistic Programs
by: Geißler, Dominik, et al.
Published: (2025)

La semiótica visual: grandes paradigmas y tendencias de línea dura
by: Jean Marie Klinkenberg
Published: (2005)

Object-Centric Conformance Alignments with Synchronization (Extended Version)
by: Gianola, Alessandro, et al.
Published: (2023)

Monitoring Data-aware Temporal Properties (Extended Version)
by: Gianola, Alessandro, et al.
Published: (2026)

Partial Incorrectness Logic
by: Verscht, Lena, et al.
Published: (2025)