?Statistical abstraction for multi-scale spatio-temporal systems? proposes a methodology that supports analysis of large-scaled spatio-temporal systems. These are represented via a set of agents whose behaviour depends on a perceived field. The proposed approach is based on a novel simulation strategy based on a statistical abstraction of the agents. The abstraction makes use of Gaussian Processes, a powerful class of non-parametric regression techniques from Bayesian Machine Learning, to estimate the agent?s behaviour given the environmental input. The authors use two biological case studies to show how the proposed technique can be used to speed up simulations and provide further insights into model behaviour. This replicated computations results report focuses on the scripts used in the paper to perform such analysis. The required software was straightforward to install and use. All the experimental results from the paper have been reproduced.
The risk posed by insider threats has usually been approached by analyzing the behavior of users solely in the cyber domain. In this paper, we show the viability of using physical movement logs, collected via a building access control system, together with an understanding of the layout of the building housing the system's assets, to detect malicious insider behavior that manifests itself in the physical domain. In particular, we propose a systematic framework that uses contextual knowledge about the system and its users, learned from historical data gathered from a building access control system, to select suitable models for representing movement behavior. We suggest two different models of movement behavior in this paper and evaluate their ability to represent normal user movement. We then explore the online usage of the learned models, together with knowledge about the layout of the building being monitored, to detect malicious insider behavior. Finally, we show the effectiveness of the developed framework using real-life data traces of user movement in railway transit stations.
Continuous-time Markov chains with alarms (ACTMCs) allow for alarm events that can be non-exponentially distributed. Within parametric ACTMCs, the parameters of alarm-event distributions are not given explicitly and can be subject of parameter synthesis. In this line, an algorithm is presented that solves the µ-optimal parameter synthesis problem for parametric ACTMCs with long-run average optimization objectives. The approach provided in this paper is based on a reduction of the problem to finding long-run average optimal policies in semi-Markov decision processes (semi-MDPs) and sufficient discretization of the parameter (i.e., action) space. Since the set of actions in the discretized semi-MDP can be very large, a straightforward approach based on an explicit action-space construction fails to solve even simple instances of the problem. The algorithm presented uses an enhanced policy iteration on symbolic representations of the action space. Soundness of the algorithm is established for parametric ACTMCs with alarm-event distributions that satisfy four mild assumptions, fulfilled by many kinds of distributions. Exemplifying proofs for the satisfaction of these requirements are provided for Dirac, uniform, exponential, Erlang, and Weibull distributions in particular. An experimental implementation shows that the symbolic technique substantially improves the efficiency of the synthesis algorithm and allows to solve instances of realistic size.
The widespread adoption of Modelling and Simulation (M&S) techniques hinges on the availability of tools supporting each phase in the M&S-based workflow. This includes tasks such as specifying, experimenting with, as well as verifying and validating simulation models. Recently, research efforts have been directed towards providing debugging support for simulation models using the same abstractions as the formalism(s) in which those models were specified. We have previously developed a technique where advanced debugging environments are generated from an explicit behavioral model of the user interface and the simulator. These models are extracted from the code of existing modelling environments and simulators, and instrumented with debugging operations. This technique can be reused for a large family of modelling formalisms. We adapt and apply this approach to accommodate dynamic-structure formalisms. As a representative example, we choose Dynamic-Structure DEVS (DSDEVS), a formalism that includes the characteristics of discrete-event and agent-based modelling paradigms. We observe that to effectively debug DSDEVS models, domain-specific visualizations developed by the modeller should be (re)used for debugging tasks. To this end, we present a modular, reusable approach, which includes an architecture and a workflow. We provide a concrete example of a minimal, but sufficiently complex simulation system modelled in the DSDEVS formalism that can be successfully debugged using the generated debugging environment.
In this paper we present Three-Valued Spatio-Temporal Logic (TSTL), which enriches the available spatio-temporal analysis of properties expressed in Signal Spatio-Temporal Logic (SSTL), to give further insight into the dynamic behaviour of systems. Our novel analysis starts from the estimation of satisfaction probabilities of given SSTL properties and allows the analysis of their temporal and spatial evolution. Moreover, in our verification procedure, we use a three-valued approach to include the intrinsic and unavoidable uncertainty related to the simulation-based statistical evaluation of the estimates; this can be also used to assess the appropriate number of simulations to use depending on the analysis needs. We present the syntax and three-valued semantics of TSTL and a specific extended monitoring algorithm to check the validity of TSTL formulas. We introduce a reliability requirement for TSTL monitoring and an automatic procedure to verify it. Two case studies demonstrate how TSTL broadens the application of spatio-temporal logics in realistic scenarios, enabling analysis of threat monitoring and privacy preservation based on spatial stochastic population models.
Accurate Modelling of a real world system with probabilistic behavior is a difficult task. Sensor noise and statistical estimations, among other errors, make the exact probability values impossible to obtain. In this paper, we consider the Interval Markov decision processes IMDPs, which generalise classical MDPs by having interval-valued transition probabilities. They provide a powerful modelling tool for probabilistic systems with an additional variation or uncertainty that prevents the knowledge of the exact transition probabilities. We investigate the problem of robust multi-objective synthesis for IMDPs and Pareto curve analysis of it. We study how to find a robust (randomized) strategy that satisfies multiple objectives involving rewards, reachability, and omega-regular properties against all possible resolutions of the transition probability uncertainties, as well as to generate an approximate Pareto curve providing an explicit view of the trade-offs between multiple objectives. We show that the multi-objective synthesis problem is PSPACE-hard and afterwards, we provide a value iteration-based decision algorithm to approximate the Pareto set of achievable points. We finally demonstrate the practical effectiveness of our proposed approaches by applying them on several case studies using a prototypical tool.
Statistical Model Checking (SMC) is an approximate verification method that overcomes the state space explosion problem for probabilistic systems by Monte Carlo simulations. Simulations might be however costly if many samples are required. It is thus necessary to implement efficient algorithms to reduce the sample size while preserving precision and accuracy. In the literature, some sequential schemes have been provided for the estimation of property occurrence based on predefined confidence and absolute or relative error. Nevertheless, these algorithms remain conservative and may result in huge sample sizes if the required precision standards are demanding. In this article, we compare some useful bounds and some sequential methods. We propose outperforming and rigorous alternative schemes, based on Massart bounds and robust confidence intervals. Our theoretical and empirical analysis show that our proposal reduces the sample size while providing guarantees on error bounds.
The existing performance evaluation methods for discrete-state stochastic models such as Petri nets either generate the reachability graph followed by a numerical solution of equations, or use some variant of simulation. Both methods have characteristic advantages and disadvantages depending on the size of the reachability graph and type of performance measure. The paper proposes a hybrid performance evaluation algorithm for Generalized Stochastic Petri Nets that integrates elements of both methods. It automatically adapts its behavior depending on the available size of main memory and number of model states. As such, the algorithm unifies simulation and numerical analysis in a joint framework. It is proved to result in an unbiased estimator whose variance tends to zero with increasing simulation time. The paper extends earlier results with an algorithm variant that starts with a small maximum number of particles and increases them during the run to increase the efficiency in cases which are rapidly solved by regular simulation. The algorithm's applicability is demonstrated through case studies.
?Analysis of spatio-temporal properties of stochastic systems using TSTL? proposes a three-valued spatio-temporal logic to enrich the analysis framework for Signal Spatio-Temporal Logic previously developed by the authors. This allows to reason on the evolution of the satisfaction of properties expressed in a spatio-temporal logic, providing additional insight on the behaviour of the studied system. The approach has been validated on two case studies: a fire spread and evacuation model, and a novel case study on privacy in a communication network. This replicated computations results report focuses on the artifact accompanying the paper, consisting of a prototypical tool implementation of the techniques presented in the paper, together with all files necessary to replicate the analysis performed thereof. The artifact is available at https://ludovicalv.github.io/TOMACS/. After a few iterations with the authors, I found that the artifact agrees with the guidelines on availability (Artifact Avaliable) and replicability (Results Replicated) dictated in https://www.acm.org/publications/policies/artifact-review-badging. The software was made available in an accessible archival repository, and thanks to the instructions provided in the accompanying webapge it has been straightforward to replicate the experimental results from the paper.
When simulating a complex stochastic system, the behavior of output response depends on input parameters estimated from finite real-world data, and the finiteness of data brings input uncertainty into the system. The quantification of the impact of input uncertainty on output response has been extensively studied. Most of the existing literature focuses on providing inferences on the mean response at the true but unknown input parameter, including point estimation and confidence interval construction. Risk quantification of mean response under input uncertainty often plays an important role in system evaluation and control, because it provides inferences on extreme scenarios of mean response in all possible input models. To the best of our knowledge, it has rarely been systematically studied in the literature. In this paper, first we introduce risk measures of mean response under input uncertainty, and propose a nested Monte Carlo simulation approach to estimate them. Then we develop asymptotical properties such as consistency and asymptotic normality for the proposed nested risk estimators. Finally we study the associated budget allocation problem for efficient nested risk simulation.