We present a new symbolic execution semantics of probabilistic programs that include observe statements and sampling from continuous distributions. Building on Kozen's seminal work, this symbolic semantics consists of a countable collection of measurable functions, along with a partition of the state space. We use the new semantics to provide a full correctness proof of symbolic execution for probabilistic programs. We also implement this semantics in the tool symProb, and illustrate its use on examples.
Phase-type distributions, the probability distributions generated by the time to absorption in a continuous-time Markov chain, are a popular tool for modeling time-dependent system behaviour. They are well understood mathematically, and so is the problem of identifying a matching distribution if given information about its moments, as well as fitting to a given distribution or a set of distribution samples. This paper looks at the problem of finding distributions from a structural perspective, namely where system behaviour is known to have a specific structure comprising parallelism, sequencing, and first-to-finish races. We present a general method that, given the coarse system structure with annotations regarding the moments of some fragments, finds a concrete phase-type distribution that fulfils the specification, if one exists. We develop the foundational underpinning in terms of constraint solving with satisfiability modulo theories, spell out the algorithmic details of a divide-and-conquer solution approach, and provide empirical evidence of feasibility, presenting a prototypical solution engine for structural distribution matching.
Improving the scalability of probabilistic model checking (PMC) tools is crucial to the verification of real-world system designs. The Stamina infinite-state PMC tool achieves scalability by iteratively constructing a partial state space for an unbounded continuous-time Markov chain model, where a majority of the probability mass resides. It then performs time-bounded transient PMC. It can efficiently produce an accurate probability bound to the property under verification. We present a new software architecture design and the C++ implementation of the Stamina 2.0 algorithm, integrated with the Storm model checker. This open-source Stamina implementation offers a high degree of modularity and provides significant optimizations to the Stamina 2.0 algorithm. Performance improvements are demonstrated on multiple challenging benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, over the previous Stamina implementation. Additionally, its design allows for future customizations and optimizations to the Stamina algorithm.
Time-sensitive networks require timely and accurate monitoring of the status of the network. To achieve this, many devices send packets periodically, which are then aggregated and forwarded to the controller. Bounding the aggregate burstiness of the traffic is then crucial for effective resource management. In this paper, we are interested in bounding this aggregate burstiness for independent and periodic flows. A deterministic bound is tight only when flows are perfectly synchronized, which is highly unlikely in practice and would be overly pessimistic. We compute the probability that the aggregate burstiness exceeds some value. When all flows have the same period and packet size, we obtain a closed-form bound using the Dvoretzky-Kiefer-Wolfowitz inequality. In the heterogeneous case, we group flows and combine the bounds obtained for each group using the convolution bound. Our bounds are numerically close to simulations and thus fairly tight. The resulting aggregate burstiness estimated for a non-zero violation probability is considerably smaller than the deterministic one: it grows in $\sqrt{n\log{n}}$, instead of $n$, where $n$ is the number of flows.
Automated synthesis of provably correct controllers for cyber-physical systems is crucial for deployment in safety-critical scenarios. However, hybrid features and stochastic or unknown behaviours make this problem challenging. We propose a method for synthesising controllers for Markov jump linear systems (MJLSs), a class of discrete-time models for cyber-physical systems, so that they certifiably satisfy probabilistic computation tree logic (PCTL) formulae. An MJLS consists of a finite set of stochastic linear dynamics and discrete jumps between these dynamics that are governed by a Markov decision process (MDP). We consider the cases where the transition probabilities of this MDP are either known up to an interval or completely unknown. Our approach is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We formalise this abstraction as an interval MDP (iMDP) for which we compute intervals of transition probabilities using sampling techniques from the so-called 'scenario approach', resulting in a probabilistically sound approximation. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
Adding probabilities to timed automata enables one to carry random simulation of their behaviors and provide answers with statistical guarantees to problems otherwise untractable. Thus, when just a timed language is given, the following natural question arises: What probability should we consider if we have no a priori knowledge except the given language and the considered length (i.e. number of events) of timed words? The maximal entropy principle tells us to take the probability measure that maximises the entropy which is the uniform measure on the language restricted to timed word of the given length (with such a uniform measure every timed word has the same chance of being sampled). The uniform sampling method developed in the last decade provides no control on the duration of sampled timed words. In the present article we consider the problem of finding a probability measure on a timed language maximising the entropy under general linear constraints on duration and for timed words of a given length. The solution we provide generalizes to timed languages a well-known result on probability measure over the real line maximising the Shannon continuous entropy under linear constraints. After giving our general theorem for general linear constraints and for general timed languages, we concentrate to the case when only the mean duration is prescribed (and again when the length is fixed) for timed languages recognised by deterministic timed automata. For this latter case, we provide an efficient sampling algorithm we have implemented and illustrated on several examples.
We present a solution to compute equilibrium probability density functions (PDFs) for the continuous component of the state in Markov regenerative processes, a class of non-Markovian processes. Equilibrium PDFs are derived as closed-form analytical expressions by applying the Key Renewal Theorem to stochastic state classes computed between regenerations. The solution, evaluated experimentally through the development of an analysis tool, provides the basis to analyze system properties from the equilibrium.
Complex models of computer systems are often difficult to study with numerical or analytical approaches because of the state space explosion problem. The class of product-form models is one of the most significant tools for overcoming this problem, and in many applications, this tool is the only way to perform a quantitative analysis. In this paper, we study the duality between two different product-form models. The first consists of a queuing network with finite capacity waiting rooms governed by the skip-over policy. The second is a recently presented product-form model in which a job fetching policy is applied. To investigate the relationships between these two models, we first extend the fetching queuing model to allow for finite capacity warehouses and for a Repetitive Service Blocking with Random Destination (RS-RD) discipline. Subsequently, we represent their distinctive features in terms of Generalized Stochastic Petri Nets which precisely specify their semantics in a modular manner and provide clear and intuitive interpretations of these policies. With these two preliminary results, we prove that it is possible to structurally transform a model of one class into one of the other and vice versa, thus choosing the representation that is computationally more convenient to compute the performance measures of interest.
Validating properties of nonlinear systems is difficult given the complexity of solving nonlinear dynamics equations. In this paper, we develop an LTL-based model checking technique to specify and validate properties of a nonlinear system. The technique can hide the difficulties in handling nonlinear difference equations, simplify the specification of properties of physical systems, and provide a high level abstraction to analyze and control nonlinear systems. We apply the proposed technique to controller synthesis problems: determining a design for a simple nonlinear control system, and finding an appropriate dosage to prescribe for drug administration.
Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. They comprise a neural ODE and a certified upper bound on the error between the abstract neural network and the concrete dynamical model. So far neural abstractions have exclusively been obtained as neural networks consisting entirely of $ReLU$ activation functions, resulting in neural ODE models that have piecewise affine dynamics, and which can be equivalently interpreted as linear hybrid automata. In this work, we observe that the utility of an abstraction depends on its use: some scenarios might require coarse abstractions that are easier to analyse, whereas others might require more complex, refined abstractions. We therefore consider neural abstractions of alternative shapes, namely either piecewise constant or nonlinear non-polynomial (specifically, obtained via sigmoidal activations). We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics. Empirically, we demonstrate the trade-off that these different neural abstraction templates have vis-a-vis their precision and synthesis time, as well as the time required for their safety verification (done via reachability computation). We improve existing synthesis techniques to enable abstraction of higher-dimensional models, and additionally discuss the abstraction of complex neural ODEs to improve the efficiency of reachability analysis for these models.
Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. Our specification language builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach considerably outperforms HyperProb, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g. partial observability) as well as inter-controller constraints (e.g. agreements on a common action).
Several notions of reversibility exist in the literature. On the one hand, causal reversibility establishes that an action can be undone provided that all of its consequences have been undone already, thereby making it possible to bring a system back to a past consistent state. On the other hand, time reversibility stipulates that the stochastic behavior of a system remains the same when the direction of time is reversed, which supports efficient performance evaluation. In this paper we show that causal reversibility is a sufficient condition for time reversibility. The study is conducted on extended labeled transition systems. Firstly, they include a forward and a backward transition relations obeying the loop property. Secondly, their transitions feature an independence relation as well as rates for their exponentially distributed random durations. Our result can thus be smoothly applied to concurrent and distributed models, calculi, and languages that account for performance aspects.
Different stochastic extensions of hybrid automata have been proposed in the past, with unclear expressivity relations between them. To structure and relate these modeling languages, in this paper we formalize two alternative approaches to extend hybrid automata with stochastic choices of discrete events and their time points. The first approach, which we call decomposed scheduling, adds stochasticity via stochastic races, choosing random time points for the possible discrete events and executing a winner with an earliest time. In contrast, composed scheduling first samples the time point of the next event and then the event to be executed at the sampled time point. We relate the two approaches regarding their expressivity and categorize available stochastic extensions of hybrid automata from the literature.
Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems that operate in the context of uncertainty or stochasticity. It builds upon ideas and techniques from a diverse range of fields, from logic, automata and graph theory, to optimisation, numerical methods and control. In recent years, probabilistic model checking has also been extended to integrate ideas from game theory, notably using models such as stochastic games and solution concepts such as equilibria, to formally verify the interaction of multiple rational agents with distinct objectives. This provides a means to reason flexibly about agents acting in either an adversarial or a collaborative fashion, and opens up opportunities to tackle new problems within, for example, artificial intelligence, robotics and autonomous systems. In this paper, we summarise some of the advances in this area, and highlight applications for which they have already been used. We discuss how the strengths of probabilistic model checking apply, or have the potential to apply, to the multi-agent setting and outline some of the key challenges required to make further progress in this field.
We present Jajapy, a Python library that implements a number of methods to aid the modelling process of Markov models from a set of partially-observable executions of the system. Currently, Jajapy supports different types of Markov models such as discrete and continuous-time Markov chains, as well as Markov decision processes. Jajapy can be used both to learn the model from scratch or to estimate parameter values of a given model so that it fits the observed data the best. To this end, the tool offers different learning techniques, either based on expectation-maximization or state-merging methods, each adapted to different types of Markov models. One key feature of Jajapy consists in its compatibility with the model checkers Storm and Prism. The paper briefly presents Jajapy’s functionalities and reports an empirical evaluation of their performance and accuracy. We conclude with an experimental comparison of Jajapy against AALpy, which is the current state-of-the-art Python library for learning automata. Jajapy and AALpy complement each other, and the choice of the library should be determined by the specific context in which it will be used.
Prism and Storm are popular model checking tools that provide a number of powerful analysis techniques for Continuous-time Markov chains (CTMCs). The outcome of the analysis is strongly dependent on the parameter values used in the model which govern the timing and probability of events of the resulting CTMC. However, for some applications, parameter values have to be empirically estimated from partially-observable executions. In this work, we address the problem of estimating parameter values of CTMCs expressed as Prism models from a number of partially-observable executions which might possibly miss some dwell time measurements. The semantics of the model is expressed as a parametric CTMC (pCTMC), i.e., CTMC where transition rates are polynomial functions over a set of parameters. Then, building on a theory of algorithms known by the initials MM, for minorization–maximization, we present an iterative maximum likelihood estimation algorithm for pCTMCs. We present an experimental evaluation of the proposed technique on a number of CTMCs from the quantitative verification benchmark set. We conclude by illustrating the use of our technique in a case study: the analysis of the spread of COVID-19 in presence of lockdown countermeasures.
We propose an approach to build and sample surrogate stochastic models leveraging state-of-the-art score-based diffusion approaches, either abstracting a known stochastic process or learning directly the model from data. In particular, we propose a method for efficient conditional sampling from such surrogate models, enforcing logical and consistency constraints on generated samples in a soft fashion. As a preliminary case study, we consider a surrogate SIR model, in both its ergodic and non-ergodic formulations. Using the aforementioned method, we are able to sample trajectories from such models that exhibit desirable features having low probability in the unconstrained models, allowing us to explore epidemiologically relevant scenarios. Although the proposed approach is still a work-in-progress, it has significant potential for applications in epidemiology and other fields. The method is also efficient in the sense that retraining is not needed to generate samples satisfying different constraints.
Various techniques have been used in recent years for verifying quantum computers, that is, for determining whether a quantum computer/system satisfies a given formal specification of correctness. Barrier certificates are a recent novel concept developed for verifying properties of dynamical systems. In this article, we investigate the usage of barrier certificates as a means for verifying behaviours of quantum systems. To do this, we extend the notion of barrier certificates from real to complex variables. We then develop a computational technique based on linear programming to automatically generate polynomial barrier certificates with complex variables taking real values. Finally, we apply our technique to several simple quantum systems to demonstrate their usage.
Safe exploration aims at addressing the limitations of Reinforcement Learning (RL) in safety-critical scenarios, where failures during trial-and-error learning may incur high costs. Several methods exist to incorporate external knowledge or to use proximal sensor data to limit the exploration of unsafe states. However, reducing exploration risks in unknown environments, where an agent must discover safety threats during exploration, remains challenging. In this paper, we target the problem of safe exploration by guiding the training with counterexamples of the safety requirement. Our method abstracts both continuous and discrete state-space systems into compact abstract models representing the safety-relevant knowledge acquired by the agent during exploration. We then exploit probabilistic counterexample generation to construct minimal simulation submodels eliciting safety requirement violations, where the agent can efficiently train offline to refine its policy towards minimising the risk of safety violations during the subsequent online exploration. We demonstrate our method’s effectiveness in reducing safety violations during online exploration in preliminary experiments by an average of 40.3% compared with QL and DQN standard algorithms and 29.1% compared with previous related work, while achieving comparable cumulative rewards with respect to unrestricted exploration and alternative approaches.
A policy that reduces communication overheads by committing together all transactions completed within an interval of time is examined. A model of the system involving two queues served alternatively with preemptions is analysed in the steady-state under Markovian assumptions. An exact and easily implementable solution is derived and is used in order to determine performance measures such as average occupancy or average latency. The optimal length of the operative interval is evaluated numerically. A non-preemptive policy is simulated and is shown to be considerably less efficient than the preemptive one analysed here. A generalization to non-Markovian operative intervals is outlined.
