Program

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 multi-objective reachability-invariant and mean-payoff queries in Markov decision processes, that is conjunctions or disjunctions either of reachability and invariant or mean-payoff 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 proof-of-concept, we report on implementations of certifying verification algorithms and experimental results.

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.

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.

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 attack-defense trees. Standard quantitative analyses available for attack-defense 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.

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 user-friendly 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 phase-type 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.

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.

In the early stages of development, parameters are useful to verify timed systems that are not fully specified and symbolic algorithms or semi-algorithms are known to compute (integer) values of the parameters ensuring some properties. They rely on the representation of the reachable state-space 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 model-checking time Petri nets, and we compare the performance of the different polyhedron and (t)PDBM-based representations of symbolic states on several classical examples from the literature.

We introduce backward dissimilarity (BD) for discrete-time 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 policy-iteration algorithm to compute BDs. Using a prototype implementation, we apply it to benchmarks from network science and discrete-time Markov chains and compare it against a related notion of bisimulation for linear control systems.

Active automata learning (AAL) can infer accurate automata models of real-time 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.

This paper presents a modal mu-calculus, $L^{rel}_{\mu,\nu}$, for encoding properties of systems modeled as timed automata. Our logic includes arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. We additionally establish that, in contrast to the other mu-calculi, $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.

Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem, and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider real-time 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 non-faulty executions w.r.t. an STL property. Thus, ? is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing ? is NP-hard in general, we provide linear-time algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response.

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 state-space. Chemical Reaction Networks (CRNs) are commonly used to describe biochemical systems. Since there are usually no upper-bounds on the population of species in a CRN, they can only be modeled as an infinite-state stochastic model. This paper proposes a new approach that can analyze infinite-state CRNs by bounding their state-space. 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 rare-event properties on a number of biochemical systems.

Non-Markovian models have great expressive power, at the cost of complex analysis of the stochastic process. The method of Stochastic State Classes (SSCs) derives closed-form 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 non-exponential 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 time-bounded transient properties of non-Markovian models. We enumerate SSCs near the root of the state-space 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.

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 non-terminating loop and with linear updates drawing from iteration-independent univariate distributions. We develop an algorithm to synthesize a probabilistic program loop given as property the close-form 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.

This paper is concerned with developing an open-source software tool, called IMPaCT, for the parallelized verification and controller synthesis of large-scale 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 infinite-horizon properties, including safety, reachability, and reach-avoid, while offering convergence guarantees. IMPaCT is developed in C++ and designed using AdaptiveCpp, an independent open-source 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 high-performance computing platforms and cloud computing services. Specifically, parallelism offered by IMPaCT effectively addresses the challenges arising from the state-explosion problem inherent in discretization-based techniques applied to large-scale stochastic systems. We benchmark IMPaCT on several physical case studies, adopted from the ARCH tool competition for stochastic models, including a 2-dimensional robot, a 3-dimensional autonomous vehicle, a 5-dimensional room temperature system, and a 7-dimensional building automation system. To show the scalability of our tool, we also employ IMPaCT for the formal analysis of a 14-dimensional case study.

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.

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 Floyd-Warshall 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.

Autonomous multi-agent 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 learning-based methods such as reinforcement learning are popular methods to train single and multi-agent autonomous systems under user-specified and state-based reward functions, applying these methods to satisfy trajectory-level task objectives is a challenging problem. In this paper, our first contribution is the use of weighted automata to specify trajectory-level objectives, such that, maximal paths induced in the weighted automaton correspond to desired trajectory-level 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 multi-agent teams targeting homogeneous task objectives. We show how shared experiences of agents and EGT-based policy updates allow us to outperform state-of-the-art RL and heuristic planning algorithms.

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 decision-making: 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 rule-of-thumb 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 twoneighboring’’’’ 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.