Checking weak observable liveness on unfoldings through asynchronous games

We define an asynchronous two-player game, played on the unfolding of a Petri net. The set of transitions of the net is partitioned among the two players, and a play is a run of the unfolding. The role of the two players is different: we assume that one of them (the User) has the right to block transitions under its control, while the other player (the System) must ensure progress of its transitions. We then define a notion of strategy for the User. In this framework, one can set different aims for the two players. Here, we consider the problem of weak observable liveness, in which the User tries to enforce liveness of a given transition. We show that a transition is weakly observably live if and only if the User has a winning strategy in the game.