ARCH-COMP18 Category Report
Stochastic Modelling
Alessandro Abate (University of Oxford)
Henk A.P. Blom (Air Transport & Operations)
Nathalie Cauchi (University of Oxford)
Sofie Haesaert (California Institute of Technology)
Arnd Hartmanns (University of Twente)
Kendra Lesser (Verus Research)
Meeko Oishi (University of New Mexico)
Vignesh Sivaramakrishnan (University of New Mexico)
Sadegh Soudjani (Newcastle University)
G.B. More Authors (External organisation)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2018. In this first edition, we present five benchmarks with different levels of complexities and stochastic favours. We make use of six different tools and frameworks (in alphabetical order): Barrier Certificates, FAUST2, FIRM-GDTL, Modest, SDCPN modelling & MC simulation and SReachTools; and attempt to solve instances of the five different benchmark problems. Through these benchmarks, we capture a snapshot on the current state-of the art tools and frameworks within the stochastic modelling domain. We also present the challenges encountered within this domain and highlight future plans which will push forward the development of more tools and methodologies for performing formal verification and optimal policy synthesis of stochastic processes.