Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking

Muhammad Osama, Anton Wijs (Corresponderende auteur)

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    2 Citaten (Scopus)

    Samenvatting

    The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. In this paper, we propose a new algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae [45] that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation with state-of-the-art LTL model checkers. Our new GPU LTL-checking algorithm is up to 150× faster on proving the correctness of a system than LTSmin running on a 32-core high-end CPU, and is more economic in using the available memory.

    Originele taal-2Engels
    TitelTools and Algorithms for the Construction and Analysis of Systems
    Subtitel30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part II
    RedacteurenBernd Finkbeiner, Laura Kovács
    Plaats van productieCham
    UitgeverijSpringer
    Pagina's23-43
    Aantal pagina's21
    ISBN van elektronische versie978-3-031-57249-4
    ISBN van geprinte versie978-3-031-57248-7
    DOI's
    StatusGepubliceerd - 5 apr. 2024
    Evenement30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 - Luxembourg City, Luxemburg
    Duur: 6 apr. 202411 apr. 2024

    Publicatie series

    NaamLecture Notes in Computer Science (LNCS)
    Volume14571
    ISSN van geprinte versie0302-9743
    ISSN van elektronische versie1611-3349

    Congres

    Congres30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024
    Land/RegioLuxemburg
    StadLuxembourg City
    Periode6/04/2411/04/24

    Vingerafdruk

    Duik in de onderzoeksthema's van 'Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit