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.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Synchronisation in Language-Level Symmetry Reduction for Probabilistic Model Checking


    Additional title:

    Lect.Notes Computer


    Contributors:

    Conference:

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


    Published in:

    Model Checking Software ; Chapter : 3 ; 49-66


    Publication date :

    2024-10-13


    Size :

    18 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Probabilistic model checking applied to autonomous spacecraft reconfiguration

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


    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


    CLOCK SYNCHRONISATION

    CATT GAVIN | European Patent Office | 2023

    Free access

    Synchronisation procedures

    Annoni, M. | SLUB | 1989


    Analysis on EURORADIO safety critical protocol by probabilistic model checking

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