Proceedings

The proceedings of QEST+FORMATS’25 are available via the links above.

Table of Contents

• A Hyperlogic for Strategies in Stochastic Games
  Lina Gerlach, Christof Löding, Erika Abraham

• Time-Sensitive Importance Splitting
  Gabriel Dengler, Carlos E. Budde, Laura Carnevali, Arnd Hartmanns

• Active Learning of Mealy Machines with Timers
  Véronique Bruyère, Bharat Garhewal, Guillermo Perez, Gaëtan Staquet, Frits Vaandrager

• Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates
  Oliver Schön, Sofie Haesaert, Sadegh Soudjani

• Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality
  Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft

• Signal Sampling and Optimisation under Symbolic Timed Automata Constraints
  Benoit Barbot, Nicolas Basset, Thao Dang, Alexandre Donzé, Marco Esposito, Dejan Nickovic

• Programming and Reasoning in Partially Observable Probabilistic Environments
  Tobias Gürtler, Benjamin Lucien Kaminski

• PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface
  Timo P. Gros, Arnd Hartmanns, Ivo Hoese, Joshua Meyer, Nicola J. Müller, Verena Wolf

• Minimal Per-Flow Backlog Bounds at an Aggregate FIFO Server under Piecewise-Linear Arrival Curves
  Lukas Wildberger, Anja Hamscher, Jens B. Schmitt

• Learning Mealy Machines with Sparse Observation Tables
  Wolffhardt Schwabe, Paul Kogel, Sabine Glesner

• What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
  Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft

• A Product-Form Model for Systems with Aging Objects and Similarities
  Andrea Marin, Diletta Olliaro, Sabina Rossi, Daniel Sadoc Menasche

• Tightening the Frontier of Decidability for Decisiveness
  Gaspard Fougea, Serge Haddad, Lina Ye, Shreyas Jain, Alain Finkel

• Fuzzy Fault Trees: The Fast and the Formal
  Thi Kim Nhung Dang, Benedikt Peterseim, Milan Lopuhaä-Zwakenberg, Mariëlle Stoelinga

• Positive Almost-Sure Termination of Polynomial Random Walks
  Lorenz Winkler, Laura Kovács

• Noninterference Analysis of Deterministically Timed Reversible Systems
  Andrea Esposito, Alessandro Aldini, Marco Bernardo

• Controller Synthesis for Parametric Timed Games
  Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Jaco van de Pol, Laure Petrucci

• Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions
  Jun Liu, Maxwell Fitzsimmons

• Using Communication to Bound Clock Drift in Local-Timed Negotiations
  Abhinav Garg, Madhavan Mukund, Adwitee Roy, B Srivathsan, Gautham Viswanathan

• Numerical Errors in Quantitative System Analysis With Decision Diagrams
  Sebastiaan Brand, Arend-Jan Quist, Richard M.K. van Dijk, Alfons Laarman

• Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata
  Pauline Blohm, Felix Schulz, Lisa Willemsen, Anne Remke, Paula Herber

• Statistical Bayesian Inference for Stochastic Process Discovery
  Paolo Ballarini, Pierre Cry, Andras Horvath, Pascale Legall

• Conservation Analysis and Discrete Probabilistic Approximations for Parameter Estimation of Biochemical Networks
  Olivier Bouët-Willaumez, Adrien Le Coënt, Benoit Barbot, Nihal Pekergin

• Formal Approximations of the Transient Distributions of the M/G/1 Workload Process
  Fabian Michel, Markus Siegle

• On Choice of Loss Functions for Neural Control Barrier Certificates
  Alireza Nadali, Ashutosh Trivedi, Majid Zamani

• Computing the Congestion Phases of Dynamical Systems with Priorities and Application to Emergency Departments
  Xavier Allamigeon, Pascal Capetillo, Stéphane Gaubert