This project has moved to GitHub and this page is no longer maintained.

ADAM (Analyzer of Distributed Asynchronous Models, in honor of Carl Adam Petri) is a synthesis tool for reactive systems with multiple independent processes. The systems are modelled as Petri games, games with one environment player and an arbitrary but bounded number of system players described as Petri nets. ADAM synthesis winning strategies of the Petri games by reducing the Petri game to a finite-graph game, solving the graph game and reconstructing the Petri game strategy from the one of the finite-graph game.

ADAM is written in Java and uses JavaBDD as library for manipulating BDDs. The APT format is used as input / output format and APT itself is used for parsing / rendering the Petri games and for providing a data structure for Petri nets. For visualizing the finite-graph games, the Petri games, and their strategies, ADAM uses the DOT format of Graphviz.

Authors: Bernd Finkbeiner, Manuel Gieseking, Ernst-Rüdiger Olderog

Documentation

• Fifth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2014) - paper
• 27th International Conference on Computer Aided Verification (CAV 2015) - paper, poster

• ReadMe
• UserGuide
• File format
• Webinterface

Files

• Executable Current version 27.10.2016 (tarball)
• Example nets (tarball)

Benchmarks

• Raw data (.zip file)
• Evaluation (.pdf file)
• Bash script for benchmark calculation (tarball)