Skip to main content

Über dieses Buch

This book constitutes the proceedings of the 15th International Conference on Quantitative Evaluation Systems, QEST 2018, held in Beijing, China, in September 2018.

The 24 full papers presented were carefully reviewed and selected from 51 submissions. The papers cover topics in the field of quantitative evaluation and verification of computer systems and networks through stochastic models and measurements emphasizing two frontier topics in research: quantitative information flow for security and industrial formal methods.



On the Additive Capacity Problem for Quantitative Information Flow

Preventing information leakage is a fundamental goal in achieving confidentiality. In many practical scenarios, however, eliminating such leaks is impossible. It becomes then desirable to quantify the severity of such leaks and establish bounds on the threat they impose. Aiming at developing measures that are robust wrt a variety of operational conditions, a theory of channel capacity for the g-leakage model was developed in [1], providing solutions for several scenarios in both the multiplicative and the additive setting.
This paper continuous this line of work by providing substantial improvements over the results of [1] for additive leakage. The main idea of employing the Kantorovich distance remains, but it is now applied to quasimetrics, and in particular the novel “convex-separation” quasimetric. The benefits are threefold: first, it allows to maximize leakage over a larger class of gain functions, most notably including the one of Shannon. Second, a solution is obtained to the problem of maximizing leakage over both priors and gain functions, left open in [1]. Third, it allows to establish an additive variant of the “Miracle” theorem from [3].
Konstantinos Chatzikokolakis

HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties

In this paper, we propose a new temporal logic for expressing and reasoning about probabilistic hyperproperties. Hyperproperties characterize the relation between different independent executions of a system. Probabilistic hyperproperties express quantitative dependencies between such executions. The standard temporal logics for probabilistic systems, i.e., PCTL and PCTL \(^*\) can refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic proposed in this paper, HyperPCTL, adds explicit and simultaneous quantification over multiple traces to PCTL. Such quantification allows expressing probabilistic hyperproperties. A model checking algorithm for the proposed logic is also introduced for discrete-time Markov chains.
Erika Ábrahám, Borzoo Bonakdarpour

How Fast Is MQTT?

Statistical Model Checking and Testing of IoT Protocols
MQTT is one of the major messaging protocols in the Internet of things (IoT). In this work, we investigate the expected performance of MQTT implementations in various settings. We present a model-based performance testing approach that allows a fast simulation of specific usage scenarios in order to perform a quantitative analysis of the latency. Out of automatically generated log-data, we learn the distributions of latencies and apply statistical model checking to analyse the functional and timing behaviour. The result is a novel testing and verification technique for analysing the performance of IoT protocols. Two well-known open source MQTT implementations are evaluated and compared.
Bernhard K. Aichernig, Richard Schumi

Parameter-Independent Strategies for pMDPs via POMDPs

Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances.
We study pMDPs with reachability objectives where the parameter values are unknown and impossible to measure directly during execution, but there is a probability distribution known over the parameter values. We study for the first time computing parameter-independent strategies that are expectation optimal, i.e., optimize the expected reachability probability under the probability distribution over the parameters. We present an encoding of our problem to partially observable MDPs (POMDPs), i.e., a reduction of our problem to computing optimal strategies in POMDPs.
We evaluate our method experimentally on several benchmarks: a motivating (repeated) learner model; a series of benchmarks of varying configurations of a robot moving on a grid; and a consensus protocol.
Sebastian Arming, Ezio Bartocci, Krishnendu Chatterjee, Joost-Pieter Katoen, Ana Sokolova

On the Verification of Weighted Kripke Structures Under Uncertainty

We study the problem of checking weighted CTL properties for weighted Kripke structures in presence of imprecise weights. We consider two extensions of the notion of weighted Kripke structures, namely (i) parametric weighted Kripke structures, having transitions weights modelled as affine maps over a set of parameters and, (ii) weight-uncertain Kripke structures, having transition labelled by real-valued random variables as opposed to precise real valued weights.
We address this problem by using extended parametric dependency graphs, a symbolic extension of dependency graphs by Liu and Smolka. Experiments performed with a prototype tool implementation show that our approach outperforms by orders of magnitude an adaptation of a state-of-the-art tool for WKSs.
Giovanni Bacci, Mikkel Hansen, Kim Guldstrand Larsen

Hospital Inventory Management Through Markov Decision Processes @runtime

Stock management in a hospital requires the achievement of a trade-off between conflicting criteria, with mandatory requirements on the quality of patient care as well as on purchasing and logistics costs. We address daily drug ordering in a ward of an Italian public hospital, where patient admission/discharge and drug consumption during the sojourn are subject to uncertainty. To derive optimal control policies minimizing the overall purchasing and stocking cost while avoiding drug shortages, the problem is modeled as a Markov Decision Process (MDP), fitting the statistics of hospitalization time and drug consumption through a discrete phase-type (DPH) distribution or a Hidden Markov Model (HMM). A planning algorithm that operates at run-time iteratively synthesizes and solves the MDP over a finite horizon, applies the first action of the best policy found, and then moves the horizon forward by one day. Experiments show the convenience of the proposed approach with respect to baseline inventory management policies.
Marco Biagi, Laura Carnevali, Francesco Santoni, Enrico Vicario

Guaranteed Error Bounds on Approximate Model Abstractions Through Reachability Analysis

It is well known that exact notions of model abstraction and reduction for dynamical systems may not be robust enough in practice because they are highly sensitive to the specific choice of parameters. In this paper we consider this problem for nonlinear ordinary differential equations (ODEs) with polynomial derivatives. We introduce approximate differential equivalence as a more permissive variant of a recently developed exact counterpart, allowing ODE variables to be related even when they are governed by nearby derivatives. We develop algorithms to (i) compute the largest approximate differential equivalence; (ii) construct an approximate quotient model from the original one via an appropriate parameter perturbation; and (iii) provide a formal certificate on the quality of the approximation as an error bound, computed as an over-approximation of the reachable set of the perturbed model. Finally, we apply approximate differential equivalences to study the effect of parametric tolerances in models of symmetric electric circuits.
Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin

Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties

Probabilistic timed automata (PTAs) are timed automata (TAs) extended with discrete probability distributions. They serve as a mathematical model for a wide range of applications that involve both stochastic and timed behaviours. In this work, we consider the problem of model-checking linear dense-time properties over PTAs. In particular, we study linear dense-time properties that can be encoded by TAs with infinite acceptance criterion. First, we show that the problem of model-checking PTAs against deterministic-TA specifications can be solved through a product construction. Based on the product construction, we prove that the computational complexity of the problem with deterministic-TA specifications is EXPTIME-complete. Then we show that when relaxed to general (nondeterministic) TAs, the model-checking problem becomes undecidable. Our results substantially extend state of the art with both the dense-time feature and the nondeterminism in TAs.
Hongfei Fu, Yi Li, Jianlin Li

Incremental Verification of Parametric and Reconfigurable Markov Chains

The analysis of parametrised systems is a growing field in verification, but the analysis of parametrised probabilistic systems is still in its infancy. This is partly because it is much harder: while there are beautiful cut-off results for non-stochastic systems that allow to focus only on small instances, there is little hope that such approaches extend to the quantitative analysis of probabilistic systems, as the probabilities depend on the size of a system. The unicorn would be an automatic transformation of a parametrised system into a formula, which allows to plot, say, the likelihood to reach a goal or the expected costs to do so, against the parameters of a system. While such analysis exists for narrow classes of systems, such as waiting queues, we aim both lower—stepwise exploring the parameter space—and higher—considering general systems.
The novelty is to heavily exploit the similarity between instances of parametrised systems. When the parameter grows, the system for the smaller parameter is, broadly speaking, present in the larger system. We use this observation to guide the elegant state-elimination method for parametric Markov chains in such a way, that the model transformations will start with those parts of the system that are stable under increasing the parameter. We argue that this can lead to a very cheap iterative way to analyse parametric systems, show how this approach extends to reconfigurable systems, and demonstrate on two benchmarks that this approach scales.
Paul Gainer, Ernst Moritz Hahn, Sven Schewe

Lumping the Approximate Master Equation for Multistate Processes on Complex Networks

Complex networks play an important role in human society and in nature. Stochastic multistate processes provide a powerful framework to model a variety of emerging phenomena such as the dynamics of an epidemic or the spreading of information on complex networks. In recent years, mean-field type approximations gained widespread attention as a tool to analyze and understand complex network dynamics. They reduce the model’s complexity by assuming that all nodes with a similar local structure behave identically. Among these methods the approximate master equation (AME) provides the most accurate description of complex networks’ dynamics by considering the whole neighborhood of a node. The size of a typical network though renders the numerical solution of multistate AME infeasible. Here, we propose an efficient approach for the numerical solution of the AME that exploits similarities between the differential equations of structurally similar groups of nodes. We cluster a large number of similar equations together and solve only a single lumped equation per cluster. Our method allows the application of the AME to real-world networks, while preserving its accuracy in computing estimates of global network properties, such as the fraction of nodes in a state at a given time.
Gerrit Großmann, Charalampos Kyriakopoulos, Luca Bortolussi, Verena Wolf

Analytical Solution for Long Battery Lifetime Prediction in Nonadaptive Systems

Uppaal SMC is a state-of-the-art tool for modelling and statistical analysis of hybrid systems, allowing the user to directly model the expected battery consumption in battery-operated devices. The tool employs a numerical approach for solving differential equations describing the continuous evolution of a hybrid system, however, the addition of a battery model significantly slows down the simulation and decreases the precision of the analysis. Moreover, Uppaal SMC is not optimized for obtaining simulations with durations of realistic battery lifetimes. We propose an analytical approach to address the performance and precision issues of battery modelling, and a trace extrapolation technique for extending the prediction horizon of Uppaal SMC. Our approach shows a performance gain of up to 80% on two industrial wireless sensor protocol models, while improving the precision with up to 55%. As a proof of concept, we develop a tool prototype where we apply our extrapolation technique for predicting battery lifetimes and show that the expected battery lifetime for several months of device operation can be computed within a reasonable computation time.
Dmitry Ivanov, Kim G. Larsen, Sibylle Schupp, Jiří Srba

Action and State Based Computation Tree Measurement Language and Algorithms

The computation tree measurement language (CTML) is a real-valued specification formalism, designed to express performance measures and dependability properties in a single framework. It is a further extension of probabilistic model checking logic in such a way that it expands the input and output value from the range of [0, 1] to the range of \([0, \infty )\). Unlike probabilistic computation tree logic (PCTL) or continuous stochastic logic (CSL), CTML can nest real values. As such, it turns out that CTML can express a nontrivial subset of probabilistic linear time logic (PLTL) formulas that cannot be expressed by PCTL while keeping the overall computational complexity being polynomial in the size of both an input formula and model. Moreover, it can express queries such as “when a message is sent, what is the expected time until it is received?” that cannot be expressed by an existing probabilistic logic, because they are“probabilistic” at most. While powerful, CTML is a state-based specification formalism. In this work, we introduce a stronger formal query language, called action and state based computation tree measurement language (asCTML). asCTML extends from CTML, for answering performance queries that operates over paths featured by a combination of states and actions. Inspired by the action and state based continuous stochastic logic (asCSL), asCTML supports multiple actions.
Yaping Jing, Andrew S. Miner

Model Checking for Safe Navigation Among Humans

We investigate the use of probabilistic model checking to synthesise optimal strategies for autonomous systems that operate among uncontrollable agents such as humans. To formally assess such uncontrollable behaviour, we use models obtained from reinforcement learning. These behaviour models are, e.g., based on data collected in experiments in which humans execute dynamic tasks in a virtual environment. We first describe a method to translate such behaviour models into Markov decision processes (MDPs). The composition of these MDPs with models for (controllable) autonomous systems gives rise to stochastic games (SGs). MDPs and SGs are amenable to probabilistic model checking which enables the synthesis of strategies that provably adhere to formal specifications such as probabilistic temporal logic constraints. Experiments with a prototype provide (1) systematic insights on the credibility and the characteristics of behavioural models and (2) methods for automated synthesis of strategies satisfying guarantees on their required characteristics in the presence of humans.
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe

Automated Verification of Concurrent Stochastic Games

We present automatic verification techniques for concurrent stochastic multi-player games (CSGs) with rewards. To express properties of such models, we adapt the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards), originally introduced for the simpler model of turn-based games, which enables quantitative reasoning about the ability of coalitions of players to achieve goals related to the probability of an event or reward measures. We propose and implement a modelling approach and model checking algorithms for property verification and strategy synthesis of CSGs, as an extension of PRISM-games. We evaluate the performance, scalability and applicability of our techniques on case studies from domains such as security, networks and finance, showing that we can analyse systems with probabilistic, cooperative and competitive behaviour between concurrent components, including many scenarios that cannot be analysed with turn-based models.
Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos

Bounded Verification of Reachability of Probabilistic Hybrid Systems

In this paper, we consider the problem of bounded reachability analysis of probabilistic hybrid systems which model discrete, continuous and probabilistic behaviors. The discrete and probabilistic dynamics are modeled using a finite state Markov decision process (MDP), and the continuous dynamics is incorporated by annotating the states of the MDP with differential equations/inclusions. We focus on polyhedral dynamical systems to model continuous dynamics. Our broad approach for computing probabilistic bounds on reachability consists of the computation of the exact minimum/maximum probability of reachability within k discrete steps in a polyhedral probabilistic hybrid system by reducing it to solving an optimization problem with satisfiability modulo theory (SMT) constraints.
We have implemented analysis algorithms in a Python toolbox, and use the Z3opt optimization solver at the backend. We report the results of experimentation on a case study involving the analysis of the probability of the depletion of the charge in a battery used in the nano-satellite.
Ratan Lal, Pavithra Prabhakar

Control and Optimization of the SRPT Service Policy by Frequency Scaling

In this paper, we study a system where the speed of a processor depends on the current number of jobs. We propose a queueing model in which jobs consist of a variable number of tasks, and priority is given to the job with the fewest remaining tasks. The number of processor frequency levels determines the dimensionality of the queueing process. The objective is to evaluate the trade-offs between holding cost and energy cost when setting the processor frequency. We obtain exact results for two and three frequency levels, and accurate approximations that can be further generalized. Numerical and simulation results show the high accuracy of the approximate solutions that we propose. Our experiments suggest that a parsimonius model with only two frequency levels is sufficient, since more elaborate models provide negligible improvements when optimizing the system.
Andrea Marin, Isi Mitrani, Maryam Elahi, Carey Williamson

Biased Processor Sharing in Fork-Join Queues

We consider a fork-join system in which a fixed amount of computational resources has to be distributed among the K tasks forming the jobs. The queueing disciplines of the fork- and join- queues are First Come First Served. At each epoch, at most K tasks are in service while the others wait in the fork-queues. We propose an algorithm with a very simple implementation that allocates the computational resources in a way that aims at minimizing the join-queue lengths, and hence at reducing the expected job service time. We study its performance in saturation and under exponential service time and provide a methodology to derive the relevant performance indices. Explicit closed-form expressions for the expected response time and join-queue length are given for the cases of jobs consisting of two, three and four tasks.
Andrea Marin, Sabina Rossi, Matteo Sottana

Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference

Probabilistic model checking for systems with large or unbounded state space is a challenging computational problem in formal modelling and its applications. Numerical algorithms require an explicit representation of the state space, while statistical approaches require a large number of samples to estimate the desired properties with high confidence. Here, we show how model checking of time-bounded path properties can be recast exactly as a Bayesian inference problem. In this novel formulation the problem can be efficiently approximated using techniques from machine learning. Our approach is inspired by a recent result in statistical physics which derived closed-form differential equations for the first-passage time distribution of stochastic processes. We show on a number of non-trivial case studies that our method achieves both high accuracy and significant computational gains compared to statistical model checking.
Dimitrios Milios, Guido Sanguinetti, David Schnoerr

LIFT: Learning Fault Trees from Observational Data

Industries with safety-critical systems increasingly collect data on events occurring at the level of system components, thus capturing instances of system failure or malfunction. With data availability, it becomes possible to automatically learn a model describing the failure modes of the system, i.e., how the states of individual components combine to cause a system failure. We present LIFT, a machine learning method for static fault trees directly out of observational datasets. The fault trees model probabilistic causal chains of events ending in a global system failure. Our method makes use of the Mantel-Haenszel statistical test to narrow down possible causal relationships between events. We evaluate LIFT with synthetic case studies, show how its performance varies with the quality of the data, and discuss practical variants of LIFT.
Meike Nauta, Doina Bucur, Mariëlle Stoelinga

A Robust Genetic Algorithm for Learning Temporal Specifications from Data

We consider the problem of mining signal temporal logical requirements from a dataset of regular (good) and anomalous (bad) trajectories of a dynamical system. We assume the training set to be labeled by human experts and that we have access only to a limited amount of data, typically noisy. We provide a systematic approach to synthesize both the syntactical structure and the parameters of the temporal logic formula using a two-steps procedure: first, we leverage a novel evolutionary algorithm for learning the structure of the formula; second, we perform the parameter synthesis operating on the statistical emulation of the average robustness for a candidate formula w.r.t. its parameters. We compare our results with our previous work [9] and with a recently proposed decision-tree [8] based method. We present experimental results on two case studies: an anomalous trajectory detection problem of a naval surveillance system and the characterization of an Ineffective Respiratory effort, showing the usefulness of our work.
Laura Nenzi, Simone Silvetti, Ezio Bartocci, Luca Bortolussi

A Hemimetric Extension of Simulation for Semi-Markov Decision Processes

Semi-Markov decision processes (SMDPs) are continuous-time Markov decision processes where the residence-time on states is governed by generic distributions on the positive real line.
In this paper we consider the problem of comparing two SMDPs with respect to their time-dependent behaviour. We propose a hemimetric between processes, which we call simulation distance, measuring the least acceleration factor by which a process needs to speed up its actions in order to behave at least as fast as another process. We show that this distance can be computed in time \(\mathcal {O}(n^2 (f(l) + k) + mn^7)\), where n is the number of states, m the number of actions, k the number of atomic propositions, and f(l) the complexity of comparing the residence-time between states. The theoretical relevance and applicability of this distance is further argued by showing that (i) it is suitable for compositional reasoning with respect to CSP-like parallel composition and (ii) has a logical characterisation in terms of a simple Markovian logic.
Mathias Ruggaard Pedersen, Giorgio Bacci, Kim Guldstrand Larsen, Radu Mardare

Policy Synthesis for Collective Dynamics

In this paper we consider the problem of policy synthesis for systems of large numbers of simple interacting agents where dynamics of the system change through information spread via broadcast communication. By modifying the existing modelling language Carma and giving it a semantics in terms of continuous time Markov decision processes we introduce a natural way of formulating policy synthesis problems for such systems. However, solving policy synthesis problems is difficult since all non-trivial models result in very large state spaces. To combat this we propose an approach exploiting the results on fluid approximations of continuous time Markov chains to obtain estimates of optimal policies.
Paul Piho, Jane Hillston

Modeling Humans: A General Agent Model for the Evaluation of Security

Careful planning is needed to design cyber infrastructures that can achieve mission objectives in the presence of deliberate attacks, including availability and reliability of service and confidentiality of data. Planning should be done with the aid of rigorous and sound security models. A security modeling formalism should be easy to learn and use, flexible enough to be used in different contexts, and should explicitly model the most significant parts of the system of interest. In particular, the research community is increasingly realizing the importance of human behavior in cyber security. However, security modeling formalisms often explicitly model only the adversary, or simplistic interactions between adversaries and defenders, or are tailored to specific use cases, or are difficult to use. We propose and define a novel security modeling formalism that explicitly models adversary, defender, and user behavior in an easy and general way, and illustrate its use with an example.
Michael Rausch, Ahmed Fawaz, Ken Keefe, William H. Sanders

Approximate Time Bounded Reachability for CTMCs and CTMDPs: A Lyapunov Approach

Time bounded reachability is a fundamental problem in model checking continuous-time Markov chains (CTMCs) and Markov decision processes (CTMDPs) for specifications in continuous stochastic logics. It can be computed by numerically solving a characteristic linear dynamical system, which is computationally expensive. We take a control-theoretic approach and propose a reduction technique that finds another dynamical system of lower dimension (number of variables), such that numerically solving the reduced dynamical system provides an approximation to the solution of the original system with guaranteed error bounds. Our technique generalises lumpability (or probabilistic bisimulation) to a quantitative setting. Our main result is a Lyapunov function characterisation of the difference in the trajectories of the two dynamics that depends on the initial mismatch and exponentially decreases over time. In particular, the Lyapunov function enables us to compute an error bound between the two dynamics as well as a convergence rate. Finally, we show that the search for the reduced dynamics can be computed in polynomial time using a Schur decomposition of the transition matrix. This enables us to efficiently solve the reduced dynamical system using exponential of upper-triangular matrices. For CTMDPs, we generalise the approach to computing a piecewise quadratic Lyapunov functions for a switched affine dynamical system. We synthesise a policy for the CTMDP via its reduced-order switched system in order to have time bounded reachability probability above a threshold. We provide error bounds that depend on the minimum dwell time of the policy. We show the efficiency of the technique on examples from queueing networks, for which lumpability does not produce any state space reduction and which cannot be solved without reduction.
Mahmoud Salamati, Sadegh Soudjani, Rupak Majumdar

On Saturation Effects in Coupled Speed Scaling

In coupled speed scaling systems, the speed of the CPU is adjusted dynamically based on the number of jobs present in the system. In this paper, we use Markov chain analysis to study the autoscaling properties of an M/GI/1/PS system. In particular, we study the saturation behaviour of the system under heavy load. Our analytical results show that the mean and variance of system occupancy are not only finite, but tightly bounded by polynomial functions of the system load and the speed scaling exponent. We build upon these results to study the speed, utilization, and mean busy period of the M/GI/1/PS. Discrete-event simulation results confirm the accuracy of our analytical models.
Maryam Elahi, Carey Williamson


Weitere Informationen

Premium Partner