Strategic (Timed) Computation Tree Logic

This repository hosts the results for the journal paper. The content has been tested on GNU/Linux and MacOS machines.

Clone this repository:

git clone --recurse-submodules https://depot.lipn.univ-paris13.fr/mosart/publications/jaamas-2024 && cd jaamas-2024

Folder Structure

.
├── case_studies        # folder containing the generated case studies
├── experiments.py      # script running the benchmarks
├── output              # folder containing the imitator's output (*unzip folder*)
├── results             # folder containing the plots and the tables of the results
└── tools               # folder containing the tools to run the benchmarks

Requirements

• python >= 3.11
• python3-pip
• antlr4
• unzip

Generate the models

The models presented in the paper can be generated using the CLI generator.py found in the folder tools/stctl.

usage: generator.py [-h] --n N [--output_folder OUTPUT_FOLDER] {philo,voter} ...

Generator of models

options:
  -h, --help            show this help message and exit
  --n N                 number of agents (default: None)
  --output_folder OUTPUT_FOLDER
                        output folder (default: .)

generators:
  {philo,voter}
    philo               generate the philosopher model
    voter               generate the voter model

For instance, the philosopher model with 5 philosophers can be generated as follows:

cd tools/stctl
python3 generator.py --n 5 --output_folder ../../case_studies philo

The voter model with 5 voters and 2 candidates can be generated as follows:

cd tools/stctl
python3 generator.py --n 5 --output_folder ../../case_studies voter --c 2

Results

1- Apply the transformation to the models

First, some Python dependencies need to be installed:

cd tools/stctl
pip3 install antlr4-python3-runtime==$(antlr4 | grep Version | awk '{print $5;}')
pip3 install -r requirements.txt

Then, it is necessary to generate the parser files:

cd tools/stctl/src
antlr4 -Dlanguage=Python3 -no-listener -visitor -o dist Imitator.g4
antlr4 -Dlanguage=Python3 -no-listener -visitor -o dist STCTL.g4

Finally, the transformation can be done with the CLI app.py found in the tools/stctl folder:

usage: app.py [-h] [--output OUTPUT] --model MODEL --property PROPERTY --method {parameters,variables} --synthesis {one,all}

STCTL

options:
  -h, --help            show this help message and exit
  --output OUTPUT       output file (default: ./output.imi)
  --model MODEL         Imitator file (default: None)
  --property PROPERTY   Property file (default: None)
  --method {parameters,variables}
                        Transformation method (default: None)
  --synthesis {one,all}
                        Sythesis method (default: None)

For instance, the following command will transform the voter model to verify the property <voter1>> EF (voter1.voted11) (file tests/examples/1-agent.stctl) in Imitator. In this case, the tool will generate the model using the method that uses variables to encode the strategies, and Imitator will synthesizes all the strategies.

python3 app.py --model ../../case_studies/voter_n5_c2.imi --property ./tests/examples/1-agent.stctl --method variables --synthesis all --output ../../case_studies/voter_n5_c2_vars.imi

The files generated are:

• ../../case_studies/voter_n5_c2_vars.imi
• ../../case_studies/1-agent_all.imiprop

2- Run the experiments

In order to run the experiments, the script experiments.py is used:

python3 experiments.py

3- Generate the figures

To install the required libraries for generating the plots, pip can be used as follows:

pip3 install -r results/requirements.txt

The folder results contains the Jupyter notebook plot.ipynb that allows interactive explore the results.

cd results && jupyter notebook

The figures can also be generated by running the script plot.py.

cd results && python3 plot.py

Note: Before running the script, the folder output must exist with the imitator's output. If you do not want to rerun the benchmark, you can decompress the existing output with:

unzip output.zip

4-Display the figures

All the generated figures can be found in the results/{model} folder. Next, we show the figures and the tables generated for the philosophers benchmark (results/philo).

Synthesising one strategy

Synthesising all strategies

Table with times (in seconds)

Authors

• Jaime Arias (LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord)
• Wojciech Jamroga (Institute of Computer Science, PAS, Warsaw University of Technology)
• Wojciech Penczek (Institute of Computer Science, PAS, Warsaw University of Technology)
• Laure Petrucci (LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord)
• Teofil Sidoruk (Institute of Computer Science, PAS, Warsaw University of Technology)

Abstract

We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e. STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for SCTL is of the same complexity as for ATLir, the model checking problem for STCTLir is of the same complexity as for TCTL, while for STCTLiR it is undecidable as for ATLiR. The above results suggest to use SCTLir and STCTLir in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTLir.