ADAM: Causality-Based Synthesis of Distributed Systems
Bernd Finkbeiner, Manuel Gieseking, and Ernst-Rüdiger Olderog
We present Adam, a tool for the automatic synthesis of distributed systems with multiple concurrent processes. For each process, an individual controller is synthesized that acts on locally available information obtained through synchronization with the environment and with other system processes. Adam is based on Petri games, an extension of Petri nets where each token is a player in a multiplayer game. Adam implements the first symbolic game solving algorithm for Petri games. We report on experience from several case studies with up to 38 system processes.
27th International Conference on Computer Aided Verification (CAV 2015).