Bounded Synthesis of Petri Games with True Concurrency Firing Semantics
Niklas Metzger
Petri games are an extension of Petri nets and synthesize causality-based distributed systems. A Petri game is a multiplayer game between the environment and the system, which has the goal to not let the environment reach bad situations. One way to find winning strategies for the system is based on bounded synthesis. In bounded synthesis, we incrementally increase the size of the strategy and can focus on small ones, which are more efficient to implement. To solve these games, we encode the behaviour of the game and the existence of a winning strategy as a quantified boolean formula (QBF). Since the search space grows exponentially, we want to reduce the size of the encoded formula. The sequential encoding describes the flow of the Petri game by interleaving the fired transitions and checking the winning conditions for a given bound. In this bachelor’s thesis, we introduce a true concurrent firing semantics on the transitions of the Petri game and extend the existing encoding to the new semantics, such that multiple transitions can be fired in one step of the encoding. With that, we can potentially speed-up the solving of the QBF, while not losing expressiveness. We prove the correctness of our approach and implement the result. A benchmark evaluation against the sequential encoding is provided.
Bachelor Thesis.