The Revised Practitioner's Guide to MDP Model Checking Algorithms

Maximilian Weininger, Arnd Hartmanns, Sebastian Junges and Tim Quatmann

Simple Linear Loops: Algebraic Invariants and Synthesis

Anton Varonka, Rida Ait El Manssour, George Kenison and Mahsa Shirmohammadi

The Threshold Problem for Hypergeometric Sequences with Quadratic Parameters

George Kenison

Exploring Consensus Robustness in Swarms with Disruptive Individuals

Julia Klein, Tatjana Petrov and Alberto D'Onofrio

Abstraction-Based Decision Making for Statistical Properties

Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner and Kaushik Mallik

Computing All Minimal Ways to Reach a Context-Free Language

Florian Bruse and Martin Lange

The Calculus of Dual Influence

Florian Bruse, Martin Lange and Sören Möller

Computing Reachable Simulations on Transition Systems

Pierre Ganty, Nicolas Manini and Francesco Ranzato

Verifying Unboundedness via Amalgamation

Ashwani Anand, Sylvain Schmitz, Lia Schütze and Georg Zetzsche

Bidding Games with Charging

Guy Avni, Ehsan Kafshdar Goharshady, Thomas A. Henzinger and Kaushik Mallik

Semi-Linear VASR for over-Approximate Semi-Linear System Reachability

Nikhil Pimpalkhare and Zachary Kincaid

On Shortest Products for Nonnegative Matrix Mortality

Andrew Ryzhikov

Programmatic Synthesis for Infinite MDPs Using Program Refinement

Joost-Pieter Katoen

Teaching Your PETS: Should I Stay or Should I Go?

Tobias Meggendorfer and Maximilian Weininger

Preservation of Rationality in Infinitary Rewriting by Top-down Tree Transducers

Munehiro Iwami and Takahito Aoto

Modelling Dynamical Systems: Learning ODEs with No Internal ODE Resolution

Bowen Zhu, Fotios Kapotos, Sida-Bastien Li, Emmanuel Goutierre, Johanne Cohen, Hayg Guler and Michèle Sébag

Smoothed Analysis of Deterministic Discounted and Mean-Payoff Games

Bruno Loff and Mateusz Skomra

Markov Decision Processes with Sure Parity and Multiple Reachability Objectives

Raphaël Berthon, Joost-Pieter Katoen and Tobias Winkler

Rollercoasters with Plateaus

Duncan Adamson, Pamela Fleischmann and Annika Huch

Hardness of Busy Beaver Value BB(15)

Tristan Stérin and Damien Woods

On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness

Misaki Kojima and Naoki Nishida

Deterministic Sub-Exponential Algorithm for Discounted-Sum Games with Unary Weights

Ali Asadi, Krishnendu Chatterjee, Jakub Svoboda and Raimundo Saona Urmeneta