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.
