ARCH-COMP22 Category Report: Stochastic Models

Alessandro Abate; Henk Blom; Joanna Delicaris; Sofie Haesaert; Arnd Hartmanns; Birgit C. van Huijgevoort; Abolfazl Lavaei; Hao Ma; Mathis Niehage; Anne Remke; Oliver Schön; Stefan  Schupp; Sadegh Soudjani; Lisa  Willemsen

doi:10.29007/lsvc

ARCH-COMP22 Category Report: Stochastic Models

Alessandro Abate, Henk Blom, Joanna Delicaris, Sofie Haesaert, Arnd Hartmanns, Birgit C. van Huijgevoort, Abolfazl Lavaei, Hao Ma, Mathis Niehage, Anne Remke, Oliver Schön, Stefan Schupp, Sadegh Soudjani, Lisa Willemsen

Research output: Contribution to journal › Article › Academic › peer-review

6 Citations (Scopus)

168 Downloads (Pure)

Abstract

This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year’s edition of the competition. In comparison with tools on non-probabilistic models, the tools for stochastic models are at the early stages of development that do not allow full competition on a standard set of benchmarks. We report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between efficiency of the implemented techniques. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2022.

Original language	English
Pages (from-to)	113-141
Number of pages	29
Journal	EPiC Series in Computing
Volume	90
DOIs	https://doi.org/10.29007/lsvc
Publication status	Published - 13 Dec 2022
Event	ARCH22 - Delft University of Technology, Delft, Netherlands Duration: 22 Aug 2022 → 24 Aug 2022

Keywords

stochastic models
Markov chains
Markov decision processes
formal verification
Control synthesis

Access to Document

10.29007/lsvc

pdfFinal published version, 674 KB

Cite this

@article{802c98167c8e413fbe253d73d3f9339a,

title = "ARCH-COMP22 Category Report: Stochastic Models",

abstract = "This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year{\textquoteright}s edition of the competition. In comparison with tools on non-probabilistic models, the tools for stochastic models are at the early stages of development that do not allow full competition on a standard set of benchmarks. We report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between efficiency of the implemented techniques. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2022.",

keywords = "stochastic models, Markov chains, Markov decision processes, formal verification, Control synthesis",

author = "Alessandro Abate and Henk Blom and Joanna Delicaris and Sofie Haesaert and Arnd Hartmanns and {van Huijgevoort}, {Birgit C.} and Abolfazl Lavaei and Hao Ma and Mathis Niehage and Anne Remke and Oliver Sch{\"o}n and Stefan Schupp and Sadegh Soudjani and Lisa Willemsen",

year = "2022",

month = dec,

day = "13",

doi = "10.29007/lsvc",

language = "English",

volume = "90",

pages = "113--141",

journal = "EPiC Series in Computing",

issn = "2398-7340",

publisher = "EasyChair",

note = "ARCH22 ; Conference date: 22-08-2022 Through 24-08-2022",

}

TY - JOUR

T1 - ARCH-COMP22 Category Report: Stochastic Models

AU - Abate, Alessandro

AU - Blom, Henk

AU - Delicaris, Joanna

AU - Haesaert, Sofie

AU - Hartmanns, Arnd

AU - van Huijgevoort, Birgit C.

AU - Lavaei, Abolfazl

AU - Ma, Hao

AU - Niehage, Mathis

AU - Remke, Anne

AU - Schön, Oliver

AU - Schupp, Stefan

AU - Soudjani, Sadegh

AU - Willemsen, Lisa

PY - 2022/12/13

Y1 - 2022/12/13

N2 - This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year’s edition of the competition. In comparison with tools on non-probabilistic models, the tools for stochastic models are at the early stages of development that do not allow full competition on a standard set of benchmarks. We report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between efficiency of the implemented techniques. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2022.

AB - This report presents the results of a friendly competition for formal verification and policy synthesis of stochastic models. It also introduces new benchmarks and their properties within this category and recommends next steps for this category towards next year’s edition of the competition. In comparison with tools on non-probabilistic models, the tools for stochastic models are at the early stages of development that do not allow full competition on a standard set of benchmarks. We report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between efficiency of the implemented techniques. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2022.

KW - stochastic models

KW - Markov chains

KW - Markov decision processes

KW - formal verification

KW - Control synthesis

UR - http://www.scopus.com/inward/record.url?scp=85148904308&partnerID=8YFLogxK

U2 - 10.29007/lsvc

DO - 10.29007/lsvc

M3 - Article

SN - 2398-7340

VL - 90

SP - 113

EP - 141

JO - EPiC Series in Computing

JF - EPiC Series in Computing

T2 - ARCH22

Y2 - 22 August 2022 through 24 August 2022

ER -

ARCH-COMP22 Category Report: Stochastic Models

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this