Tools at the Frontiers of Quantitative Verification

• DOI: 10.48550/arxiv.2405.13583
• Publication Date: 2024-05-22
• Authors: Roman Andriushchenko; Alexander Bork; Carlos E. Budde; Milan Češka; Kush Grover; Ernst Moritz Hahn; Arnd Hartmanns; Bryant Israelsen; 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
• Keywords: FOS: Computer and information sciences; Computer Science - Logic in Computer Science; Logic in Computer Science (cs.LO)

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