Towards End-to-End GPU Acceleration of PCTL Model Checking

Jan Heemstra, Muhammad Osama, Anton Wijs

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademicpeer review

    Samenvatting

    So far, existing probabilistic model checkers have been programmed to run on a CPU. While earlier work has accelerated some procedures of model checking with GPUs, such as matrix-vector multiplication for probabilistic model checking, we are the first to construct an end-to-end GPU-accelerated probabilistic model checker, where every step of the model checking process, from constructing a Discrete-Time Markov Chain to the verification of a Probabilistic Computation Tree Logic (PCTL) formula, occurs on the GPU, and where all relevant data is located in GPU memory. In this paper, we discuss the challenges imposed by the GPU architecture and memory constraints and how we overcame them, present intermediate performance results for a supported fragment of PCTL, and discuss the challenges that remain to support full PCTL property checking.

    Originele taal-2Engels
    TitelLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    UitgeverijSpringer
    Pagina's314-337
    Aantal pagina's24
    DOI's
    StatusGepubliceerd - 2025

    Publicatie series

    NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume15261 LNCS
    ISSN van geprinte versie0302-9743
    ISSN van elektronische versie1611-3349

    Bibliografische nota

    Publisher Copyright:
    © The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.

    Vingerafdruk

    Duik in de onderzoeksthema's van 'Towards End-to-End GPU Acceleration of PCTL Model Checking'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit