README.md

Strategic (Timed) Computation Tree Logic

This repository hosts the results for the 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
├── results             # folder containing the results of the benchmark
├── run_experiments.sh  # script running the benchmark
└── tools               # folder containing the tools to generate the case studies

Requirements

• python >= 3.11
• pip
• antlr4

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 case_studies/1-voter.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 ../../case_studies/1-voter.stctl --method variables --synthesis all --output ../../case_studies/voter_n5_c2_vars.imi

2- Run the experiments

In order to run the experiments, the script run_experiments.sh is used as follows:

./run_experiments.sh -v <number_of_voters> -a <number_of_agents> -c <number_of_candidates> -s <type_of_strategy> -o <output_name>.csv

where -v is the number of voters, -a the number of agents, -c the number of candidates, -s the type of strategy, and -o the filename where the results will be saved.

The help of the script can be displayed with the -h option.

./run_experiments.sh -h

usage: ./run_experiments.sh [-h | [-v maxvoters] [-a maxagents] [-c maxcandidates] [-s one|all] [-t timeout] -o table_filename]

Executes the experiments.
The result is written in the file specified with the -o option

  -h                This help
  -v maxvoters      Uses a specified value for the maximal number of voters [default: 3]
  -a maxagents      Uses a specified value for the maximal number of agents [default: 2]
  -c maxcandidates  Uses a specified value for the maximal number of candidates [default: 4]
  -s strategy       Find one strategy or all of them [default: one]
  -t timeout        Uses a specified value for the timeout (in seconds) [default: 120]

To reproduce the results presented in the paper, the commands to execute are the following:

# model-checking
./run_experiments.sh -v 15 -a 3 -c 4 -s one -o results_one.csv

# synthesising all strategies
./run_experiments.sh -v 5 -a 3 -c 4 -s all -o results_all.csv

Display 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

Model Checking

Synthesising all strategies

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.