Skip to main content

ARCH−COMP18 Category Report: Stochastic Modelling

Alessandro Abate‚ Henk Blom‚ Nathalie Cauchi‚ Sofie Haesaert‚ Arnd Hartmanns‚ Kendra Lesser‚ Meeko Oishi‚ Vignesh Sivaramakrishnan‚ Sadegh Soudjani‚ Cristian−Ioan Vasile and Abraham P. Vinod

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 flavours. 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.

Book Title
ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems
Editor
Goran Frehse
Journal
EPiC Series in Computing
Pages
71 − 103
Publisher
EasyChair
Volume
54
Year
2018