ACM Transactions on Modeling and Computer Simulation
- New York : Association for Computing Machinery (ACM), 2021
- [various pagings] : illustrations, 26 cm.
Includes bibliographical references.
State-space Construction of Hybrid Petri Nets with Multiple Stochastic Firings -- A Modest Approach to Markov Automata -- Transfer Reinforcement Learning for Autonomous Driving: From WiseMove to WiseSim -- Doping Tests for Cyber-physical Systems -- Replication of Computational Results Report for "Doping Tests for Cyber-Physical Systems" -- Falsification of Hybrid Systems Using Adaptive Probabilistic Search.
[Article Title: State-space Construction of Hybrid Petri Nets with Multiple Stochastic Firings/ Jannik H├╝ls, Carina Pilch, Patricia Schinke, Henner Niehaus, Joanna Delicaris and Anne Remke, p. 13:1-13:37] Abstract: Hybrid Petri nets have been extended to include general transitions that fire after a randomly distributed amount of time. With a single general one-shot transition the state space and evolution over time can be represented either as a Parametric Location Tree or as a Stochastic Time Diagram. Recent work has shown that both representations can be combined and then allow multiple stochastic firings. This work presents an algorithm for building the Parametric Location Tree with multiple general transition firings and shows how its transient probability distribution can be computed using multi-dimensional integration. We discuss the (dis-)advantages of an interval arithmetic and a geometric approach to compute the areas of integration. Furthermore, we provide details on how to perform a Monte Carlo integration either directly on these intervals or convex polytopes, or after transformation to standard simplices. A case study on a battery-backup system shows the feasibility of the approach and discusses the performance of the different integration approaches.;[Article Title: A Modest Approach to Markov Automata/ Yuliya Butkova, Arnd Hartmanns and Holger Hermanns, p. 14:1-14:34] Abstract: Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In this article, we present extensions to MODEST, an expressive high-level language with roots in process algebra, that allow large Markov automata models to be specified in a succinct, modular way. We illustrate the advantages of MODEST over alternative languages. Model checking Markov automata models requires dedicated algorithms for time-bounded and long-run average reward properties. We describe and evaluate the state-of-the-art algorithms implemented in the mcsta model checker of the MODEST TOOLSET. We find that mcsta improves the performance and scalability of Markov automata model checking compared to earlier and alternative tools. We explain a partial-exploration approach based on the BRTDP method designed to mitigate the state space explosion problem of model checking, and experimentally evaluate its effectiveness. This problem can be avoided entirely by purely simulation-based techniques, but the nondeterminism in Markov automata hinders their straightforward application. We explain how lightweight scheduler sampling can make simulation possible, and provide a detailed evaluation of its usefulness on several benchmarks using the MODEST TOOLSET's modes simulator.;[Article Title: Transfer Reinforcement Learning for Autonomous Driving: From WiseMove to WiseSim/ Aravind Balakrishnan, Jaeyoung Lee, Ashish Gaurav, Krzysztof Czarnecki and Sean Sedwards, p. 15:1-15:26] Abstract: Reinforcement learning (RL) is an attractive way to implement high-level decision-making policies for autonomous driving, but learning directly from a real vehicle or a high-fidelity simulator is variously infeasible. We therefore consider the problem of transfer reinforcement learning and study how a policy learned in a simple environment using WiseMove can be transferred to our high-fidelity simulator, WiseMove. WiseMove is a framework to study safety and other aspects of RL for autonomous driving. WiseMove accurately reproduces the dynamics and software stack of our real vehicle. We find that the accurately modelled perception errors in WiseMove contribute the most to the transfer problem. These errors, when even naively modelled in WiseMove, provide an RL policy that performs better in WiseMove than a hand-crafted rule-based policy. Applying domain randomization to the environment in WiseMove yields an even better policy. The final RL policy reduces the failures due to perception errors from 10% to 2.75%. We also observe that the RL policy has significantly less reliance on velocity compared to the rule-based policy, having learned that its measurement is unreliable.;[Article Title: Doping Tests for Cyber-physical Systems/ Sebastian Biewer, Pedro R. D'argenio and Holger Hermanns, p. 16:1-16:27] Abstract: The software running in embedded or cyber-physical systems is typically of proprietary nature, so users do not know precisely what the systems they own are (in)capable of doing. Most malfunctionings of such systems are not intended by the manufacturer, but some are, which means these cannot be classified as bugs or security loopholes. The most prominent examples have become public in the diesel emissions scandal, where millions of cars were found to be equipped with software violating the law, altogether polluting the environment and putting human health at risk. The behaviour of the software embedded in these cars was intended by the manufacturer, but it was not in the interest of society, a phenomenon that has been called software doping. Due to the unavailability of a specification, the analysis of doped software is significantly different from that for buggy or insecure software and hence classical verification and testing techniques have to be adapted. The work presented in this article builds on existing definitions of software doping and lays the theoretical foundations for conducting software doping tests, so as to enable uncovering unethical manufacturers. The complex nature of software doping makes it very hard to effectuate doping tests in practice. We explain the main challenges and provide efficient solutions to realise doping tests despite this complexity.;[Article Title: Replication of Computational Results Report for "Doping Tests for Cyber-Physical Systems"/ Gerrit Grossmann, p. 17:1-17:2] Abstract: The article Doping Tests for Cyber-Physical Systems is accompanied by a prototype implementation in Python 2.7. The artifact (i.e., code and observational data) is hosted on a publicly available repository. The article contains comprehensive documentation in the appendix, and running the code is straightforward. The article Doping Tests for Cyber-Physical Systems can thus receive the Artifacts Evaluated-Reusable badge. ;[Article Title: Falsification of Hybrid Systems Using Adaptive Probabilistic Search/ Gidon Ernst, Sean Sedwards, Zhenya Zhang and Ichiro Hasuo, p. 18:1-18:22] Abstract: We present and analyse an algorithm that quickly finds falsifying inputs for hybrid systems. Our method is based on a probabilistically directed tree search, whose distribution adapts to consider an increasingly fine-grained discretization of the input space. In experiments with standard benchmarks, our algorithm shows comparable or better performance to existing techniques, yet it does not build an explicit model of a system. Instead, at each decision point within a single trial, it makes an uninformed probabilistic choice between simple strategies to extend the input signal by means of exploration or exploitation. Key to our approach is the way input signal space is decomposed into levels, such that coarse segments are more probable than fine segments. We perform experiments to demonstrate how and why our approach works, finding that a fully randomized exploration strategy performs as well as our original algorithm that exploits robustness. We propose this strategy as a new baseline for falsification and conclude that more discriminative benchmarks are required.