Skip to content
Snippets Groups Projects
Select Git revision
  • 24e71f31777fa28a57a178cc658db7744e00a2db
  • main default protected
2 results

restarting-markov-chains-experiments

  • Clone with SSH
  • Clone with HTTPS
    • Vincent Grande's avatar
    added funding
    Vincent Grande authored
    24e71f31
    History
    Vincent Grande's avatar 24e71f31
    History
    Name Last commit Last update
    PRISM
    .gitignore
    ExperimentsBlackBoxStorm.ipynb
    ExperimentsPopulationProtocolsAll.ipynb
    README.md
    avc93g.json
    avc_17_8.json
    avc_9_3_typo.json
    avc_typo_17_8.json
    majority.json
    majority_broken.json
    README.md

    Restarting Markov Chains Experiments

    Main Paper

    The main paper "Black-box Testing Liveness Properties of Partially Observable Stochastic Systems", Javier Esparza and Vincent P. Grande, can be found under https://drops.dagstuhl.de/storage/00lipics/lipics-vol261-icalp2023/LIPIcs.ICALP.2023.126/LIPIcs.ICALP.2023.126.pdf

    Dependencies

    In addition to standard python Packages, the experiments require an installation of the Storm Model Checker and Stormpy Python interface:

    https://moves-rwth.github.io/stormpy/

    Experiments

    The Population Protocol Experiments can be found in one Notebook, and the other experiments in the other. We use the descriptions of the Population protocols generated by Peregrine https://peregrine.model.in.tum.de , and altered instances of the PRISM Benchmark suite, with the experimental settings taken over from the two papers mentioned in our paper.

    Multiprocessing

    The experiments make use of multiprocessing by default. Please adjust the number of cores used to your preferences. The Notebooks have been tested on a MacBook Pro 2021 with a 10 core M1 Pro Processor and 32 GB of RAM, and a Linux server with 2*16 core Intel Xeon with 768 GB of RAM.

    Funding

    Javier Esparza: Partially funded by the DFG within Research Training Group 2428 CONVEY. Vincent P. Grande: Funded by the DFG (German Research Foundation) under Research Training Group 2236/2 UnRAVeL.