In Petri games, the places of an underlying Petri net are distinguished into environment and system places. Environment and system players are represented by tokens residing on these respective places. Players are not informed of each others moves unless they engage in a joint transition. Then they exchange their causal history as formalized by the unfolding of the Petri game. We consider safety objectives, where the goal of the system players is to avoid certain bad places despite of the environment's move. A strategy for the system players is obtained by restricting the choices in the unfolding so that these bad places are avoided, but also no deadlock occurs.
We present a logic for describing knowledge of players in Petri games. To this end, we extend ideas from event structure logic for describing partial oder structures as introduced by Wojciech Penczek as well as M. Mukund and P.S. Thiagarajan in the 1990s. In event structure logic, causality, conflict, and concurrency can be directly expressed. We instantiate these concepts in the setting of unfoldings of Petri games. Our extensions to event structure logic concern quantification over labels and a knowledge operator. The aim is to apply this logic for a compositional rely-guarantee reasoning about strategies for Petri games.
(Joint work with Bernd Finkbeiner)