QEST+FORMATS Program

I0		Wednesday		Thursday		Friday

8:30	On now Registration & Coffee	On now Registration & Coffee	On now Registration & Coffee





9:00	On now QEST+FORMATS Opening Session chair: Mingshuai Chen & Max Tschaikowski Q+F	On now Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A	On now Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A

9:10	On now Monitoring of Timed and Quantitative Systems Session chair: Mingshuai Chen Kim G. Larsen Q+F









10:00		On now Coffee Break	On now Coffee Break

10:10	On now Coffee Break



10:30	On now Q+F Session 1 - Markov Models under Uncertainty Session chair: Martin Fränzle Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov ChainsPeter Buchholz Wasserstein error bounds for aggregations of continuous-time Markov chainsFabian Michel Robust Parameter Learning for Uncertain MDPsYannik Schnitzer, Alessandro Abate, David Parker	On now Q+F Session 4 - Stochastic Model Checking Session chair: Peter Buchholz Multi-Objective Statistical Model Checking using Lightweight Strategy SamplingPedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk Effective Stochastic Automata Model Checking by Interval AbstractionAnnabell Petri, Arnd Hartmanns, Pedro D'Argenio Collective Decision-Making Under Timing ConstraintsJulia Klein, Tatjana Petrov	On now Q+F Session 7 - Dependability and Security Analysis Session chair: Arnd Hartmanns Facing the Core: State-Space Compression of Dynamic Fault Trees via PH-DistributionsNazareno Garagiola, Holger Hermanns Adaptive Importance Sampling for Static Fault Trees with Two-State Markovian ComponentsLeonardo Paroli, Laura Carnevali, Enrico Vicario The Cost of Repetition: A Compositional Scalability Model for Attack TreesClemens Fruböse, Eva Hetzel

















12:00	On now Lunch	On now Lunch	On now Lunch

















13:30	On now Supporting Older Adults Living Independently Session chair: Andrea Vandin Jane Hillston Q+F	On now Q+F Session 5 - Probabilistic and Temporal Logic Semantics Session chair: Jane Hillston Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic DecompositionMohamed Hamza Bandukara, Fredrik Dahlqvist, Niki Omidvari Algebraic Robust Semantics for Signal Temporal Logic with Graph OperatorsSheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann, Jyotirmoy Deshmukh	On now Q+F Session 8 - Queueing and Performance Models Session chair: Enrico Vicario Stationary Analysis of Finite-Capacity M/M/1 Fork-Join QueuesPierre Fiorini The Component Queues Method for Quasi-Birth-Death Process Fitting and AnalysisJulianna Bor, Giuliano Casale, Evgenia Smirni











14:30	On now Coffee Break	On now Coffee Break	On now Coffee Break





15:00	On now Q+F Session 2 - Parametric Games and Automata Session chair: Masaki Waga State-Space Abstractions for Parametric Timed GamesMikael Bisgaard Dahlsen-Jensen, Jaco van de Pol, Laure Petrucci Verification of parametric Markov Automata under time-bounded reachabilityKevin van de Glind, Matthias Volk, Tim Willemse	On now Q+F Session 6 - Continuous and Hybrid Systems Session chair: Tatjana Petrov Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step AdaptationMikkel Bjørn, Daniel Hansen, Grace Melchiors, Kim Guldstrand Larsen, Christian Schilling Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal LogicLena Becker, Holger Hermanns	On now Q+F Session 9 - Timed Automata and Languages Session chair: Marco Bernardo Weighing Timed Regular Languages: The Final StepEugene Asarin, Aldric Degorre, Catalin Dima, Bernardo Jacobo Inclán Witnesses and Counterexamples for Timed BisimulationAlexander Lieb, Malte Lochau











16:00	On now Coffee Break		On now Coffee Break





16:30	On now Q+F Session 3 - Learning and Quantum Systems Session chair: Kim G. Larsen Learning Alternating Real-Time AutomataKazuki Kinoshita, Masaki Waga Faster algorithm for achieving minimal-size quantum decision diagramsJuul Sanders, Sebastiaan Brand, Tim Coopmans		On now Q+F Session 10 - Verification Tools Session chair: Eugene Asarin MightyPPL: Towards model checking MTLHsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh Pandya LF-mc: An Efficient Verifier for Lingua FrancaMario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function SynthesisRayan Mazouz, Frederik Mathiesen, Luca Laurenti, Morteza Lahijanian











		19:00 Social Dinner & Cruise (Boarding at 7:15pm)	18:00 Football

Wednesday

8:30	On now Registration & Coffee
9:00	On now QEST+FORMATS Opening Session chair: Mingshuai Chen & Max Tschaikowski Q+F
9:10	On now Monitoring of Timed and Quantitative Systems Session chair: Mingshuai Chen Kim G. Larsen Q+F
10:10	On now Coffee Break
10:30	On now Q+F Session 1 - Markov Models under Uncertainty Session chair: Martin Fränzle Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov Chains Peter Buchholz Wasserstein error bounds for aggregations of continuous-time Markov chains Fabian Michel Robust Parameter Learning for Uncertain MDPs Yannik Schnitzer, Alessandro Abate, David Parker
12:00	On now Lunch
13:30	On now Supporting Older Adults Living Independently Session chair: Andrea Vandin Jane Hillston Q+F
14:30	On now Coffee Break
15:00	On now Q+F Session 2 - Parametric Games and Automata Session chair: Masaki Waga State-Space Abstractions for Parametric Timed Games Mikael Bisgaard Dahlsen-Jensen, Jaco van de Pol, Laure Petrucci Verification of parametric Markov Automata under time-bounded reachability Kevin van de Glind, Matthias Volk, Tim Willemse
16:00	On now Coffee Break
16:30	On now Q+F Session 3 - Learning and Quantum Systems Session chair: Kim G. Larsen Learning Alternating Real-Time Automata Kazuki Kinoshita, Masaki Waga Faster algorithm for achieving minimal-size quantum decision diagrams Juul Sanders, Sebastiaan Brand, Tim Coopmans

Thursday

8:30	On now Registration & Coffee
9:00	On now Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	On now Coffee Break
10:30	On now Q+F Session 4 - Stochastic Model Checking Session chair: Peter Buchholz Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk Effective Stochastic Automata Model Checking by Interval Abstraction Annabell Petri, Arnd Hartmanns, Pedro D'Argenio Collective Decision-Making Under Timing Constraints Julia Klein, Tatjana Petrov
12:00	On now Lunch
13:30	On now Q+F Session 5 - Probabilistic and Temporal Logic Semantics Session chair: Jane Hillston Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition Mohamed Hamza Bandukara, Fredrik Dahlqvist, Niki Omidvari Algebraic Robust Semantics for Signal Temporal Logic with Graph Operators Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann, Jyotirmoy Deshmukh
14:30	On now Coffee Break
15:00	On now Q+F Session 6 - Continuous and Hybrid Systems Session chair: Tatjana Petrov Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation Mikkel Bjørn, Daniel Hansen, Grace Melchiors, Kim Guldstrand Larsen, Christian Schilling Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic Lena Becker, Holger Hermanns
19:00	On now Social Dinner & Cruise (Boarding at 7:15pm)

Friday

8:30	On now Registration & Coffee
9:00	On now Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	On now Coffee Break
10:30	On now Q+F Session 7 - Dependability and Security Analysis Session chair: Arnd Hartmanns Facing the Core: State-Space Compression of Dynamic Fault Trees via PH-Distributions Nazareno Garagiola, Holger Hermanns Adaptive Importance Sampling for Static Fault Trees with Two-State Markovian Components Leonardo Paroli, Laura Carnevali, Enrico Vicario The Cost of Repetition: A Compositional Scalability Model for Attack Trees Clemens Fruböse, Eva Hetzel
12:00	On now Lunch
13:30	On now Q+F Session 8 - Queueing and Performance Models Session chair: Enrico Vicario Stationary Analysis of Finite-Capacity M/M/1 Fork-Join Queues Pierre Fiorini The Component Queues Method for Quasi-Birth-Death Process Fitting and Analysis Julianna Bor, Giuliano Casale, Evgenia Smirni
14:30	On now Coffee Break
15:00	On now Q+F Session 9 - Timed Automata and Languages Session chair: Marco Bernardo Weighing Timed Regular Languages: The Final Step Eugene Asarin, Aldric Degorre, Catalin Dima, Bernardo Jacobo Inclán Witnesses and Counterexamples for Timed Bisimulation Alexander Lieb, Malte Lochau
16:00	On now Coffee Break
16:30	On now Q+F Session 10 - Verification Tools Session chair: Eugene Asarin MightyPPL: Towards model checking MTL Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh Pandya LF-mc: An Efficient Verifier for Lingua Franca Mario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis Rayan Mazouz, Frederik Mathiesen, Luca Laurenti, Morteza Lahijanian
18:00	On now Football

Caption

Invited

Q+F