Program
Awards
Approximation of Cumulative Distribution Functions by Bernstein Phase Type Distributions András Horváth, Illés Horváth, Marco Paolieri, Miklós Telek and Enrico Vicario 

Efficiently Computable DistanceBased Robustness for a Practical Fragment of STL Neha Rino, Mohammed Foughali and Eugene Asarin 

Transient Evaluation of NonMarkovian Models by Stochastic State Classes and Simulation Gabriel Dengler, Laura Carnevali, Carlos E. Budde and Enrico Vicario 

Certificates and Witnesses for MultiObjective Queries in Markov Decision Processes Christel Baier, Calvin Chau and Sascha Klüppelholz 
Sessions
Date  Time  Session  Description 

20240910  08:50  09:00  Opening  presentations 
09:00  10:00  Invited talk by Mor HarcholBalter  presentations  
10:00  10:30  Coffee Break  coffee break  
10:30  12:00  Understanding Systems  presentations  
12:00  13:30  Lunch Break  lunch  
13:30  15:00  Input Modelling and Parameterisation  presentations  
15:00  15:30  Coffee Break  coffee break  
18:00  20:00  Reception  (to be confirmed)  
20240911  09:00  10:00  Invited talk by Corina Pasareanu  presentations 
10:00  10:30  Coffee Break  coffee break  
10:30  12:00  Timed Systems  presentations  
12:00  13:30  Lunch Break  lunch  
13:30  15:00  Temporal Logic + work in progress  presentations  
15:00  15:30  Coffee Break  coffee break  
15:30  17:00  Rare events + work in progress  presentations  
18:00  20:00  Banquet  first nations performance followed by dinner  
20240912  09:00  10:00  Invited talk by Thomas Wies (CONCUR)  presentations 
10:00  10:30  Coffee Break  coffee break  
10:30  12:00  Program and Controller Synthesis  presentations  
12:00  13:30  Lunch Break  lunch  
13:30  15:00  MDP and Weighted Automata  presentations  
15:00  15:30  Coffee Break  coffee break  
15:30  17:00  Tool demo session  tool demonstrations 
Talks
Understanding Systems

20240910, 10:3011:00
Certificates and Witnesses for MultiObjective Queries in Markov Decision Processes
Sascha Klüppelholz, Calvin Chau🎤 and Christel BaierAbstract
Certifying verification algorithms not only return whether a given property holds or not, but also provide an accompanying independently checkable certificate and a corresponding witness. The certificate can be used to easily validate the correctness of the result and the witness provides useful diagnostic information, e.g. for debugging purposes. Thus, certificates and witnesses substantially increase the trustworthiness and understandability of the verification process. In this work, we consider certificates and witnesses for multiobjective reachabilityinvariant and meanpayoff queries in Markov decision processes, that is conjunctions or disjunctions either of reachability and invariant or meanpayoff predicates, both universally and existentially quantified. Thereby, we generalize previous works on certificates and witnesses for single reachability and invariant constraints. To this end, we turn known linear programming techniques into certifying algorithms and show that witnesses in the form of schedulers and subsystems can be obtained. As a proofofconcept, we report on implementations of certifying verification algorithms and experimental results.

20240910, 11:0011:30
Diagnosis of Stochastic Systems: Optimising Costs and Delays
Isaline Plaid , Engel Lefaucheux and Marie DuflotAbstract
Diagnosing a partially observable stochastic system consists in telling, based on the actions observed along a path, whether the system has encountered an (unobservable) event called fault. Several notions of diagnosability have been studied in this context depending on whether an (arbitrarily small) error probability is tolerated upon claiming a fault or not. Choosing which events can effectively be observed through sensors has a strong impact on diagnosis. With more observable events a given system is in general more likely to be diagnosable, and in case it is diagnosable it is more likely to detect a fault sooner. However, detecting events can have a cost, for instance in terms of sensors needed to detect those events. In this paper we tackle both diagnosability notions while restricting the set of observable events. First we try to balance costs and diagnosability, studying whether a system is diagnosable with less than N observable events. Then we study the latency of diagnosis, a measure that computes the mean time to wait between the occurrence of a fault and the moment when it is detected. We also consider two types of masks: static ones in which the set of observable events is fixed, and dynamic masks for which the set of observable events can evolve along an execution, based on what has been observed so far.

20240910, 11:3012:00
A framework for optimisation based stochastic process discovery
Pascale Le Gall , Pierre Cry , Andras Horvath and Paolo BallariniAbstract
Process mining is concerned with deriving formal models capable of reproducing the behaviour of a given organisational process by analysing observed executions collected in an event log. The elements of an event log are finite sequences (i.e., traces or words) of actions. Many effective algorithms have been introduced which issue a control flow model (commonly in Petri net form) aimed at reproducing, as precisely as possible, the language of the considered event log. However, given that identical executions can be observed several times, traces of an event log are associated with a frequency and, hence, an event log inherently yields also a stochastic language. By exploiting the trace frequencies contained in the event log, the stochastic extension of process mining, therefore, consists in deriving stochastic (Petri nets) models capable of reproducing the likelihood of the observed executions. In this paper, we introduce a novel stochastic process mining approach. Starting from a ``standard’’’’ Petri net model mined through classical mining algorithms, we employ optimization to identify optimal weights for the transitions of the mined net so that the stochastic language issued by the stochastic interpretation of the mined net closely resembles that of the event log. The optimization is either based on the maximum likelihood principle or on the earth moving distance. Experiments on some popular real system logs show an improved accuracy w.r.t. to alternative approaches.
Input Modelling and Parameterisation

20240910, 13:3014:00
QuADTool: AttackDefenseTree Synthesis, Analysis and Bridge to Verification
Jan Kretinsky , Julia Eisentraut and Florian DorfhuberAbstract
Ranking risks and countermeasures is one of the foremost goals of quantitative security analysis. One of the popular frameworks, used also in industrial practice, for this task are attackdefense trees. Standard quantitative analyses available for attackdefense trees can distinguish likely from unlikely vulnerabilities. We provide a tool that allows for easy synthesis and analysis of those models. The later including the domains of probabilities, cost and time. Furthermore, it provides a variety of interfaces to existing model checkers and analysis tools. Unfortunately, currently available tools rely on precise quantitative inputs (probabilities, timing, or costs of attacks), which are rarely available. Instead, only statistical, imprecise information is typically available, leaving us with probably approximately correct (PAC) estimates of the real quantities. As a part of our tool, we extend the standard analysis techniques so they can handle the imprecise, PAC input and yield rigorous bounds on the imprecision and uncertainty of the final result of the analysis.

20240910, 14:0014:30
Adaption of Stochastic Models (ASMo)  A Tool for Input Modeling 
Alina Timmermann , Alexander Puzicha , Andreas Blume , Falko Bause and Peter BuchholzAbstract
Analysis of trace data and modeling of data by appropriate distributions are essential for constructing accurate stochastic models. However, software support for these tasks is fragmented across various tools and libraries, including but not limited to tools like ExpertFit, MATLAB, R or software libraries like pystats. This dispersion of software components can be challenging for users who lack experience with these software packages and requires, even for experienced users, a huge effort to configure adequate tool chains for data analysis and modeling. This paper introduces the first version of the ASMo tool, designed to collect various techniques for data analysis and modeling under a userfriendly umbrella. ASMo consolidates different data inspection and fitting approaches into a single platform, simplifying the process for modelers. It offers support for data inspection, analysis, calculation, and visualization of various statistical measures. Additionally, ASMo provides fitting algorithms for standard, mixture, and phasetype distributions and can directly export random variate generators for the fitted distributions. ASMo is intended as an open environment which can be easily extended by integrating new methods.

20240910, 14:3015:00
Approximation of Cumulative Distribution Functions by Bernstein Phase Type Distributions
Illes Horvath , Enrico Vicario, Miklos Telek, Marco Paolieri and András HorváthAbstract
A typical problem in stochastic analyses is to include in the model arbitrarily distributed random variables. This is often tackled by choosing a parametric family of distributions and apply fitting algorithms to find appropriate parameters. In a recent paper it was shown that ap proximating a probability density function (PDF) by Bernstein expo nentials, which are obtained from Bernstein polynomials by a change of variable, results in a particular case of acyclic phase type distributions (that we will call Bernstein phase type distributions). In this paper we show that this approach can also be based on cumulative distribution functions (CDFs) and using CDFs in the approximation has some ad vantages over using PDFs.
Timed Systems

20240911, 10:3011:00
On Parametric DBMs and their applications to time Petri nets
Olivier H. Roux, Didier Lime and Loriane LeclercqAbstract
In the early stages of development, parameters are useful to verify timed systems that are not fully specified and symbolic algorithms or semialgorithms are known to compute (integer) values of the parameters ensuring some properties. They rely on the representation of the reachable statespace as convex polyhedra. In the case of Parametric Timed Automata or Parametric Time Petri Nets (PTPN), those convex polyhedra have a special form that can be represented with a dedicated data structure called Parametric Difference Bound Matrices (PDBM). Surprisingly few results are available for PDBMs, so we take a fresh look at them and show how they can be computed efficiently in PTPNs. In the process, we define tropical PDBMs (tPDBMs) that generalize the original definition and allows, in contrast to that former definition, to avoid splitting the represented polyhedra. We argue in particular that while tPDBMs are more costly to handle than their split counterpart, they allow for better convergence. We have implemented both versions in Roméo, our tool for modelchecking time Petri nets, and we compare the performance of the different polyhedron and (t)PDBMbased representations of symbolic states on several classical examples from the literature.

20240911, 11:0011:30
Dissimilarity for Linear Dynamical Systems
Andrea Vandin, Max Tschaikowski, Mirco Tribastone, Giuseppe Squillace , Kim Guldstrand Larsen, Giovanni Bacci and Giorgio BacciAbstract
We introduce backward dissimilarity (BD) for discretetime linear dynamical systems (LDS), which relaxes existing notions of bisimulations by allowing for approximate comparisons. BD is an invariant property stating that the difference along the evolution of the dynamics governing two state variables is bounded by a constant, which we call dissimilarity. We demonstrate the applicability of BD in a simple case study and showcase its use concerning: (i) robust model comparison; (ii) approximate model reduction; and (iii) approximate data recovery. Our main technical contribution is a policyiteration algorithm to compute BDs. Using a prototype implementation, we apply it to benchmarks from network science and discretetime Markov chains and compare it against a related notion of bisimulation for linear control systems.

20240911, 11:3012:00
MMLT/ik: Efficiently Learning Mealy Machines with Local Timers by using Imprecise Symbol Filters
Sabine Glesner , Wolffhardt Schwabe and Paul KogelAbstract
Active automata learning (AAL) can infer accurate automata models of realtime systems (RTS). However, even efficient AAL methods for RTS, like learning Mealy machines with local timers (MMLTs), take very long to infer models with large input alphabets. We introduce MMLT/ik, a method for learning accurate MMLTs fast by ignoring transitions based on imprecise prior knowledge (ik) from an imprecise symbol filter. We validate our method across a diverse set of case studies with automotive system components, network protocols, wireless sensor networks, and smart home appliances, where we reduce runtime drastically.
Temporal Logic + work in progress

20240911, 13:3014:00
An Expressive Timed Modal MuCalculus for Timed Automata
Peter Fontana, Jeroen J.A. Keiren and Rance CleavelandAbstract
This paper presents a modal mucalculus, $L^{rel}_{\mu,\nu}$, for encoding properties of systems modeled as timed automata. Our logic includes arbitrary fixpoints and an untillike modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mucalculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional regiongraph construction for timed automata. We additionally establish that, in contrast to the other mucalculi, $L^{rel}_{\mu,\nu}$ is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for $L^{rel}_{\mu,\nu}$ are immediately usable as model checkers for TCTL for general timed automata.

20240911, 14:0014:30
Efficiently Computable DistanceBased Robustness for a Practical Fragment of STL
Eugene Asarin , Mohammed Foughali and Neha RinoAbstract
Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the statespace explosion problem, and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole statespace and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider realtime systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure ? for STL, based on a new distance that we define over timed signals. In contrast with existing measures, ? provides a precise quantification of distances between the monitored signal and the boundary separating faulty and nonfaulty executions w.r.t. an STL property. Thus, ? is suitable for a wide range of reallife perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing ? is NPhard in general, we provide lineartime algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response.

20240911, 14:3014:45
REDUCTO: A novel approach to the reduction of Boolean Networks
Andrea Vandin🎤Abstract
Model reduction is a pressing need in many areas of science and engineering due to the socalled ‘curse of dimensionality’. In this talk, I will review recent reduction techniques for Boolean Networks (BN), a wellestablished popular model in biology proposed in the 60s. The results were obtained within the Danish DFF RP1 project “REDUCTO: A novel approach to the reduction of Boolean Networks” started in 2020 and ended in late 2023. REDUCTO succeeded in creating reduction techniques for BNs demonstrating high reduction power and high analysis speed ups on many models from the literature, while preserving exactly dynamics of interest. These results are based on key notions of computer science such as quantitative bisimulation, and satisfiability modulo theory. Using a prototype implementation of our minimization algorithms, we found reductions on more than 60 BN from two wellknown repositories, leading to analysis speedups in practice. This is based on joint work with Alberto Lluch Lafuente, Mirco Tribastone, and Max Tschaikowski.

20240911, 14:4515:00
Hyperproperties for Privacy, Fairness, and Legal Requirements
Ashutosh Trivedi🎤Abstract
In recent years, the study of hyperproperties has offered insights into complex system behaviors, yet many practical fields remain unexplored territories for these concepts. This talk aims to highlight the connection between hyperproperty research and realworld applications, drawing from my work in related domains such as cyberphysical systems (CPS), software fairness, legal compliance, and metamorphic testing. I will illustrate how concepts developed for hyperproperties can be effectively applied to ensure system confidentiality, equitable outcomes, regulatory adherence, and robust software testing. By exploring these practical settings, I hope to invite formal methods researchers to venture into new areas, offering fresh challenges and groundbreaking possibilities for the application of their innovative research. Join me as we discuss these diverse fields, uncovering the potential for hyperproperties to revolutionize approaches and solutions across various disciplines.
Rare Events + work in progress

20240911, 15:3016:00
RareEvent Guided Analysis of InfiniteState Chemical Reaction Networks
Hao Zheng and Mohammad AhmadiAbstract
Probabilistic Model Checking (PMC) is a valuable tool for automated analysis of systems exhibiting stochastic behavior. However, the effectiveness of PMC algorithms is limited to systems that can be modeled by a finite statespace. Chemical Reaction Networks (CRNs) are commonly used to describe biochemical systems. Since there are usually no upperbounds on the population of species in a CRN, they can only be modeled as an infinitestate stochastic model. This paper proposes a new approach that can analyze infinitestate CRNs by bounding their statespace. For a property indicating that the probability of the event of interest is less than a certain threshold value, the objective is to generate a bounded range on the population of each species in the CRN such that this bounded CRN already retains sufficient probability to refute the property under investigation. The effectiveness of this approach is demonstrated by analyzing rareevent properties on a number of biochemical systems.

20240911, 16:0016:30
Transient Evaluation of NonMarkovian Models by Stochastic State Classes and Simulation
Enrico Vicario, Carlos E. Budde , Laura Carnevali and Gabriel DenglerAbstract
NonMarkovian models have great expressive power, at the cost of complex analysis of the stochastic process. The method of Stochastic State Classes (SSCs) derives closedform analytical expressions for the joint Probability Density Functions (PDFs) of the active timers with marginal expolynomial PDF, though being hindered by the number of concurrent nonexponential timers and of discrete events between regenerations. Simulation is an alternative capable of handling the large class of PDFs samplable via inverse transform, which however suffers from rare events. We combine these approaches to analyze timebounded transient properties of nonMarkovian models. We enumerate SSCs near the root of the statespace tree and then rely on simulation to reach the target, affording transient evaluation of models for which the method of SSCs is not viable while reducing computational time and variance of the estimator of transient probabilities with respect to simulation. Promising results are observed in the estimation of rare event probabilities.

20240911, 16:3016:45
PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems
Ben Wooding🎤Abstract
We are developing an opensource software tool, called PRoTECT, for safety barrier certificates (BCs) for nonlinear polynomial systems using sumofsquares (SOS) optimization. PRoTECT supports four classes of dynamical systems: (i) discretetime stochastic systems, (ii) discretetime deterministic systems, (iii) continuoustime stochastic systems, and (iv) continuoustime deterministic systems. PRoTECT is implemented in Python and can be used via an application programming interface (API) or a userfriendly graphic user interface (GUI). Additionally, PRoTECT enables parallelism over different barrier degrees to efficiently search for a feasible BC. We wish to discuss how well PRoTECT might fit with existing workflows to be of benefit to researchers. Extensions could include support for datadriven methods and controller design.
Program and Controller Synthesis

20240912, 10:3011:00
Probabilistic Loop Synthesis from Sequences of Moments
Ezio Bartocci and Miroslav StankovicAbstract
Probabilistic program synthesis consists in automatically creating programs that generating random values adhering to specified distributions. We consider here the class of probabilistic programs with a potentially nonterminating loop and with linear updates drawing from iterationindependent univariate distributions. We develop an algorithm to synthesize a probabilistic program loop given as property the closeform expressions of the first three statistical moments in the number of loop iterations. Our approach supports random draws from Gaussian, discrete, or a combination of discrete and continuous distributions. We demonstrate the effectiveness of our approach through various case studies.

20240912, 11:0011:30
IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of LargeScale Stochastic Systems
Abolfazl Lavaei and Ben WoodingAbstract
This paper is concerned with developing an opensource software tool, called IMPaCT, for the parallelized verification and controller synthesis of largescale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs), respectively. The tool serves to (i) construct IMCs/IMDPs as finite abstractions of underlying original systems, and (ii) leverage interval iteration algorithms for formal verification and controller synthesis over infinitehorizon properties, including safety, reachability, and reachavoid, while offering convergence guarantees. IMPaCT is developed in C++ and designed using AdaptiveCpp, an independent opensource implementation of SYCL, for adaptive parallelism over CPUs and GPUs of all hardware vendors, including Intel and NVIDIA. IMPaCT stands as the first software tool for the parallel construction of IMCs/IMDPs, empowered with the capability to leverage highperformance computing platforms and cloud computing services. Specifically, parallelism offered by IMPaCT effectively addresses the challenges arising from the stateexplosion problem inherent in discretizationbased techniques applied to largescale stochastic systems. We benchmark IMPaCT on several physical case studies, adopted from the ARCH tool competition for stochastic models, including a 2dimensional robot, a 3dimensional autonomous vehicle, a 5dimensional room temperature system, and a 7dimensional building automation system. To show the scalability of our tool, we also employ IMPaCT for the formal analysis of a 14dimensional case study.

20240912, 11:3012:00
Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards
Youssouf Oualhadj, Catalin Dima, Damien BusattoGaston and Benoit BarbotAbstract
We consider the synthesis problem on timed automata with Büchi objectives, where delay choices made by a controller are perturbed by a small amount. Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we extend existing results to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation. In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the region abstraction, and generalizes previous characterization of winning cycles in the absence of punctual guards. We show that the problem remains within PSPACE despite the presence of punctual guards.
MDP and Weighted Automata

20240912, 13:3014:00
A FloydWarshall Approach to Value Computation in Markov Decision Processes
Loic Helouet, Eric Fabre and Aymeric ComeAbstract
Standard value and policy iteration approaches in MDP alternatively optimize the values of sates and policies building on the values computed at a previous iteration, until convergence. This paper revisits iterative approaches: We show that the values under a policy can be computed as discounted weights in weighted automata. The weight of infinite cycles can be obtained as fixpoints of dedicated operators. Values are obtained by integration over paths via an adaptation of FloydWarshall algorithm. We first define an algebraic framework to compute the actual value of a MDP. It can be easily adapted to compute other quantities such as the variance of value in a MDP. We then run experiments to study convergence of value calculus, and show that in many models, convergence is achieved before integration of all paths. This opens the way to new approximation and optimization schemes for value calculus.

20240912, 14:0014:30
Multi Agent Pathfinding for Timed Tasks using Evolutionary Techniques
Jyotirmoy Deshmukh, Xin Qin , Anand Balakrishnan and Sheryl PaulAbstract
Autonomous multiagent systems such as hospital robots and package delivery drones often operate in highly uncertain environments and are expected to achieve complex temporal task objectives while ensuring safety. While learningbased methods such as reinforcement learning are popular methods to train single and multiagent autonomous systems under userspecified and statebased reward functions, applying these methods to satisfy trajectorylevel task objectives is a challenging problem. In this paper, our first contribution is the use of weighted automata to specify trajectorylevel objectives, such that, maximal paths induced in the weighted automaton correspond to desired trajectorylevel behaviors. We show how weighted automata based specifications go beyond timeliness properties focused on deadlines to performance properties such as expeditiousness. Our second contribution is the use of evolutionary game theory (EGT) principles to train homogeneous multiagent teams targeting homogeneous task objectives. We show how shared experiences of agents and EGTbased policy updates allow us to outperform stateoftheart RL and heuristic planning algorithms.

20240912, 14:3015:00
What is your discount factor?
Ashutosh Trivedi, Sriram Sankaranarayanan and Shadi Tasdighi KalatAbstract
Discounted reward is a canonical objective in sequential optimization, reinforcement learning, and algorithmic game theory. The popularity of discounted reward in these mathematical tools can be attributed to the theoretical elegance rendered by discounting in producing a contraction improvement mapping. Moreover, other natural optimization objectives such as total reward and average reward can be mimicked by discounted reward with a sufficiently large discount factor. At the same time, the practical success of discounted reward is due to its naturalness in formalizing a myopic view of the future by rational agents when faced with sequential decisionmaking: a dollar today is worth more than a dollar tomorrow. The decay in the value of a dollar is captured by the discount factor, but it is difficult to pinpoint the value of a discount factor that an agent may subscribe to. In the absence of such a value, modelers often resort to using ruleofthumb discount factors close to 1. Besides being disconnected from actual time preference, such discount factors frequently cause convergence problems in learning scenarios. This paper focuses on the problem of eliciting the exact range of discount factors for a rational agent by observing their behavior. We investigate how an agent’’s discount factor can be inferred by observing their behavior given as a policy on a finite Markov decision process (MDP). We employ the notion of
optimum policy regions'''' for discount factors and characterize the intervals where the optimum policies remain invariant. The boundaries of such intervals are points at which two
neighboring’’’’ optimum policies have the same value. Therefore, the range of discount factors for which a given policy is optimal is identified by points where its value intersects with the value of neighboring optimum policies. We develop numerical approaches to compute these boundary points under different assumptions on the optimality of the policy. We demonstrate the effectiveness of our algorithms through some case studies.