Certificates and Witnesses for Multi-objective ω-Regular Queries in Markov Decision Processes

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

Abstract

Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustworthiness and explainability of model checking tools, we present independently checkable certificates and witnesses for multi-objective ω-regular queries in Markov decision processes. For the certification, we extend and improve existing certificates for the decomposition of maximal end components and reachability properties. We then derive mixed-integer linear programs (MILPs) for finding minimal witnessing subsystems. For the special case of Markov chains and LTL properties, we use unambiguous Büchi automata to find witnesses, resulting in an algorithm that requires single-exponential space. Existing approaches based on deterministic automata require doubly-exponential space in the worst case. Finally, we consider the practical computation of our certificates and witnesses and provide an implementation of the developed techniques, along with an experimental evaluation, demonstrating the efficacy of our techniques.

Details

Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
EditorsDomenico Bianculli, Elena Gomez-Martinez
PublisherSpringer, Cham
Pages129-147
Number of pages19
ISBN (electronic)978-3-032-10444-1
ISBN (print)978-3-032-10443-4
Publication statusPublished - 12 Nov 2025
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science
Volume16192 LNCS
ISSN0302-9743

Conference

Title23rd International Conference on Software Engineering and Formal Methods
Abbreviated titleSEFM 2025
Conference number23
Duration10 - 14 November 2025
Website
LocationUniversity of Castilla-La Mancha
CityToledo
CountrySpain

External IDs

ORCID /0000-0002-5321-9343/work/205988102
ORCID /0000-0003-1724-2586/work/205991657
ORCID /0000-0002-3437-0240/work/205992907

Keywords

Keywords

  • Certificates, Markov decision process, Multi-objective