Strategic (Timed) Computation Tree Logic

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

Clone this repository:

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

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

Results

Compilation of the generator

Firstly, please compile the models generator as follows:

cd tools/voters_generator
make

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.