wovepaper — the arXiv observatory

The paper identifies flaws in a previous modular rule for proving almost‑sure termination of probabilistic programs and introduces a sound modular rule based on descent supermartin…

Publications (137)

What is Decidable about Partially Observable Markov Decision Processes with Ï-Regular Objectives

Conditionally Optimal Algorithms for Generalized BÃ¼chi Games

Strategy Improvement for Concurrent Safety Games

Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information

On Memoryless Quantitative Objectives

The Complexity of Coverage

Deciding Fast Termination for Probabilistic VASS with Nondeterminism

Computation Tree Logic for Synchronization Properties

The Complexity of Ergodic Mean-payoff Games

Doomsday Equilibria for Omega-Regular Games

Decidable Problems for Probabilistic Automata on Infinite Words

Modular Verification for Almost-Sure Termination of Probabilistic Programs

GIST: A Solver for Probabilistic Games

Non-polynomial Worst-Case Analysis of Recursive Programs

Strategy complexity of finite-horizon Markov decision processes and simple stochastic games

Approximating the minimum cycle mean

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

Coverability: Realizability Lower Bounds

POMDPs under Probabilistic Semantics

Strong Amplifiers of Natural Selection: Proofs

The Complexity of Synthesis from Probabilistic Components

Magnifying Lens Abstraction for Stochastic Games with Discounted and Long-run Average Objectives

An O(n^2) Time Algorithm for Alternating BÃ¼chi Games

Synthesis of AMBA AHB from Formal Specification

Faster Algorithms for Algebraic Path Properties in RSMs with Constant Treewidth

CEGAR for Qualitative Analysis of Probabilistic Systems

Strategy Representation by Decision Trees in Reactive Synthesis

Faster Algorithms for Mean-Payoff Parity Games

Robustness of Structurally Equivalent Concurrent Parity Games

Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with BÃ¼chi Objectives

Bounded Rationality in Concurrent Parity Games

Optimizing Expectation with Guarantees in POMDPs (Technical Report)

Nested Weighted Limit-Average Automata of Bounded Width

The Complexity of Partial-observation Stochastic Parity Games With Finite-memory Strategies

Mean-payoff Automaton Expressions

Forgiver triumphs in alternating Prisoner's Dilemma

Markov Decision Processes with Multiple Long-run Average Objectives

Partial-Observation Stochastic Games: How to Win when Belief Fails

Robust Draws in Balanced Knockout Tournaments

POMDPs under Probabilistic Semantics

Energy and Mean-Payoff Parity Markov Decision Processes

Probabilistic Systems with LimSup and LimInf Objectives

The Complexity of Multi-Mean-Payoff and Multi-Energy Games

Qualitative Analysis of POMDPs with Temporal Logic Specifications for Robotics Applications

Optimal Cost Almost-sure Reachability in POMDPs

Data-centric Dynamic Partial Order Reduction

Termination Analysis of Probabilistic Programs through Positivstellensatz's

Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis

Fixation probability and fixation time in structured populations

Infinite-state games with finitary conditions

Qualitative Analysis of Concurrent Mean-payoff Games

Stochastic Limit-Average Games are in EXPTIME

Measuring and Synthesizing Systems in Probabilistic Environments

Counterexample Explanation by Learning Small Strategies in Markov Decision Processes

Algorithms for Game Metrics

Strategy Improvement for Concurrent Reachability and Safety Games

A reduction from parity games to simple stochastic games

Edit Distance for Pushdown Automata

Secure Credit Reporting on the Blockchain

Strategy Synthesis for Multi-dimensional Quantitative Objectives

Mean-Payoff Pushdown Games

Randomness for Free

Expressiveness and Closure Properties for Quantitative Languages

Stochastic Shortest Path with Energy Constraints in POMDPs

Algorithms for BÃ¼chi Games

Expressiveness and Closure Properties for Quantitative Languages

Assume-Guarantee Synthesis for Digital Contract Signing

Quantitative Synthesis for Concurrent Programs

Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS

Looking at Mean-Payoff and Total-Payoff through Windows

Cost Analysis of Nondeterministic Probabilistic Programs

Energy Parity Games

Finitary languages

Strategy Complexity of Concurrent Stochastic Games with Safety and Reachability Objectives

Improved Algorithms for Parity and Streett objectives

Lower Bounds for Symbolic Computation on Graphs: Strongly Connected Components, Liveness, Safety, and Diameter

MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives

Model and Objective Separation with Conditional Lower Bounds: Disjunction is Harder than Conjunction

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

What is Decidable about Partially Observable Markov Decision Processes with Ï-Regular Objectives