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