The generic representatives (or counter abstraction) approach has been shown to be an effective symmetry reduction method for model checking. This method was extended to a probabilistic setting via a specialised language, Symmetric Probabilistic Specification Language (SPSL) and an associated tool, GRIP, for use with the PRISM model checker. However, SPSL does not support synchronisation-based communication, making this method inapplicable to systems that require synchronisation. We show how synchronisation can be added to SPSL, and develop new counter abstraction translation rules for synchronous statements. We extend GRIP accordingly and demonstrate the feasibility and effectiveness of the new abstraction rules via a range of examples. This extends the applicability of the generic representatives technique to the wide class of probabilistic systems that rely on synchronisation. Experimental results show that our approach works well for systems that are composed of a large number of simple symmetric modules that feature a small amount of synchronisation-based communication.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking


    Weitere Titelangaben:

    Lect.Notes Computer


    Beteiligte:
    Neele, Thomas (Herausgeber:in) / Wijs, Anton (Herausgeber:in) / Valkov, Ivaylo (Autor:in) / Donaldson, Alastair F. (Autor:in) / Miller, Alice (Autor:in)

    Kongress:

    International Symposium on Model Checking Software ; 2024 ; Luxembourg City, Luxembourg April 10, 2024 - April 11, 2024


    Erschienen in:

    Model Checking Software ; Kapitel : 3 ; 49-66


    Erscheinungsdatum :

    13.10.2024


    Format / Umfang :

    18 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Probabilistic model checking applied to autonomous spacecraft reconfiguration

    Nardone, Vittoria / Santone, Antonella / Tipaldi, Massimo et al. | IEEE | 2016


    CLOCK SYNCHRONISATION

    CATT GAVIN | Europäisches Patentamt | 2023

    Freier Zugriff

    Synchronisation procedures

    Annoni, M. | SLUB | 1989


    Performance Evaluation of Metro Regulations Using Probabilistic Model-Checking

    Bertrand, Nathalie / Bordais, Benjamin / Hélouët, Loïc et al. | British Library Conference Proceedings | 2019


    Analysis on EURORADIO safety critical protocol by probabilistic model checking

    Quan, Hongyu / Zhao, Huibing / Zhou, Guo | IEEE | 2013