ARCH-COMP23 Category Report: Stochastic Models

Alessandro Abate; Henk Blom; Nathalie Cauchi; Joanna Delicaris; Sofie Haesaert; Birgit van Huijgevoort; Abolfazl Lavaei; Anne Remke; Oliver Schön; Stefan Schupp; Fedor Shmarov; Sadegh Soudjani; Lisa Willemsen; Paolo Zuliani

doi:10.29007/k7s6

Research output: Contribution to journal › Conference article › peer-review

67 Downloads (Pure)

Abstract

This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. Given that the tools for stochastic models are at their early stages of development compared to those of non-probabilistic models, the main focus is to report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between the efficiency of the implemented techniques. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2023.

Original language	English
Pages (from-to)	126-150
Number of pages	25
Journal	EPiC Series in Computing
Volume	96
DOIs	https://doi.org/10.29007/k7s6
Publication status	Published - 2023
Event	10th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2023 - San Antonio, United States Duration: 9 May 2023 → 9 May 2023

Keywords

control synthesis
formal verification
Markov chains
Markov Decision Processes
stochastic models

Access to Document

10.29007/k7s6

pdfFinal published version, 701 KB

Cite this

@article{58c059fd164542da8607c34e1b49ca41,

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

abstract = "This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year{\textquoteright}s edition of the competition. Given that the tools for stochastic models are at their early stages of development compared to those of non-probabilistic models, the main focus is to report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between the efficiency of the implemented techniques. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2023.",

keywords = "control synthesis, formal verification, Markov chains, Markov Decision Processes, stochastic models",

author = "Alessandro Abate and Henk Blom and Nathalie Cauchi and Joanna Delicaris and Sofie Haesaert and \{van Huijgevoort\}, Birgit and Abolfazl Lavaei and Anne Remke and Oliver Sch{\"o}n and Stefan Schupp and Fedor Shmarov and Sadegh Soudjani and Lisa Willemsen and Paolo Zuliani",

year = "2023",

doi = "10.29007/k7s6",

language = "English",

volume = "96",

pages = "126--150",

journal = "EPiC Series in Computing",

issn = "2398-7340",

publisher = "EasyChair",

note = "10th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2023 ; Conference date: 09-05-2023 Through 09-05-2023",

}

TY - JOUR

T1 - ARCH-COMP23 Category Report

T2 - 10th International Workshop on Applied Verification of Continuous and Hybrid Systems, ARCH 2023

AU - Abate, Alessandro

AU - Blom, Henk

AU - Cauchi, Nathalie

AU - Delicaris, Joanna

AU - Haesaert, Sofie

AU - van Huijgevoort, Birgit

AU - Lavaei, Abolfazl

AU - Remke, Anne

AU - Schön, Oliver

AU - Schupp, Stefan

AU - Shmarov, Fedor

AU - Soudjani, Sadegh

AU - Willemsen, Lisa

AU - Zuliani, Paolo

PY - 2023

Y1 - 2023

N2 - This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. Given that the tools for stochastic models are at their early stages of development compared to those of non-probabilistic models, the main focus is to report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between the efficiency of the implemented techniques. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2023.

AB - This report is concerned with a friendly competition for formal verification and policy synthesis of stochastic models. The main goal of the report is to introduce new benchmarks and their properties within this category and recommend next steps toward next year’s edition of the competition. Given that the tools for stochastic models are at their early stages of development compared to those of non-probabilistic models, the main focus is to report on an initiative to collect a set of minimal benchmarks that all such tools can run, thus facilitating the comparison between the efficiency of the implemented techniques. This friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in Summer 2023.

KW - control synthesis

KW - formal verification

KW - Markov chains

KW - Markov Decision Processes

KW - stochastic models

UR - https://www.scopus.com/pages/publications/85188193557

U2 - 10.29007/k7s6

DO - 10.29007/k7s6

M3 - Conference article

AN - SCOPUS:85188193557

SN - 2398-7340

VL - 96

SP - 126

EP - 150

JO - EPiC Series in Computing

JF - EPiC Series in Computing

Y2 - 9 May 2023 through 9 May 2023

ER -

ARCH-COMP23 Category Report: Stochastic Models

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this