Pith. sign in

REVIEW 1 cited by

Tools at the Frontiers of Quantitative Verification

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2405.13583 v1 pith:WFAD43ZP submitted 2024-05-22 cs.LO

Roman Andriushchenko , Alexander Bork , Carlos E. Budde , Milan Češka , Kush Grover , Ernst Moritz Hahn , Arnd Hartmanns , Bryant Israelsen
show 15 more authors
Nils Jansen Joshua Jeppson Sebastian Junges Maximilian A. Köhl Bettina Könighofer Jan Křetínský Tobias Meggendorfer David Parker Stefan Pranger Tim Quatmann Enno Ruijters Landon Taylor Matthias Volk Maximilian Weininger Zhen Zhang
This is my paper · ORCID
classification cs.LO
keywords quantitativemodelstoolsverificationadvancedsupporttoolanalysis
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet

    cs.AI 2024-11 conditional novelty 2.0 of 10

    This paper is a tutorial survey of robust MDPs, covering semantics, dynamic programming algorithms, model connections, applications, and open challenges.

Pith tools