Decentralized Multi-Agent Strategy Synthesis under LTLf Specifications via Exchange of Least-Limiting Advisers
This repository provides implementation and case studies for the paper "Decentralized Multi-Agent Strategy Synthesis under LTLf Specifications via Exchange of Least-Limiting Advisers"
We use MONA to convert LTLf formulae to DFA. Check the website for installation instructions or try to install with apt.
sudo apt install mona
PRISM-games is used for all computations on stochastic games. We recommend building from source, please check their website for build instructions.
We use Py4J to create a java gateway in order to access the PRISM-games java API. You need to expand the java classpath to include PRISM .class files and .jars. Check the PRISM-api github for further examples and information.
pip3 install py4j
pygame is used for visualization purposes.
pip3 install networkx ltlf2dfa pygame
In order to run the code, first start the java PRISM handler. Make sure your classpath includes py4j and the PRISM-games .class files and .jars either by extending the CLASSPATH or using the -cp option.
cd prismhandler
javac PrismEntryPoint.java
java PrismEntryPoint.java
Once the gateway is running, run the main code or the unittests:
python3 main.py