imitator/aamas2026 repository overview

IMITATOR4AMAS supports model checking and synthesis of memoryless imperfect information strategies for STCTL, interpreted over networks of parametric timed automata with asynchronous execution. While extending the verifier IMITATOR, IMITATOR4AMAS is the first tool for strategy synthesis in this setting. Our experimental results show a substantial speedup over previous approaches.

To replicate the experiments, install the latest Docker package and run the following commands (tested under Ubuntu 22.04 running via WSL, and on MacOS). The imitator/aamas2026 container should be automatically downloaded the first time docker run is called.

Voters example:

docker run imitator/aamas2026 /imitator/examples/voters.imi /imitator/examples/voters.imiprop -no-var-autoremove

Treasure hunters example:

docker run imitator/aamas2026 /imitator/examples/treasure_clocks.imi /imitator/examples/treasure.imiprop -no-var-autoremove

Conference example:

docker run imitator/aamas2026 /imitator/examples/conf2.imi /imitator/examples/conf2.imiprop -no-var-autoremove

Linux environment:

To access the source files of the tool and of the examples, you can run docker so as to work in a linux environment:

docker run --rm -it --entrypoint "/bin/bash" -v YOUR_LOCAL_EXAMPLES_DIRECTORY:/COPY_IN_THE_IMAGE -w /imitator imitator/aamas2026

Where the following options are used:

--rm: clean the container files when exiting

-it: interactive usage with a terminal window

--entrypoint "/bin/bash": run the shell when starting the container instead of the imitator tool

-v YOUR_LOCAL_EXAMPLES_DIRECTORY:/COPY_IN_THE_IMAGE: if you want to make your own examples, you can link their folder on your own machine with a folder in the docker image that is run. You can then easily edit them as usual on your machine and test them in the docker image. Then replace YOUR_LOCAL_EXAMPLES_DIRECTORY with the path to your folder, and COPY_IN_THE_IMAGE with the name in the docker. It will be found (because of the /) at the root of the directories tree.

If you don't plan to use this possibility, just remove this option from the command line.

-w /imitator: the working directory where you start. If you are using the previous option, you could write -w /COPY_IN_THE_IMAGE to work directly in the folder of your own files.

The tool is then run, as in the video, using e.g.:

/imitator/bin/imitator /imitator/examples/treasure_clocks.imi /imitator/examples/treasure.imiprop -no-var-autoremove