Weak observable liveness and infinite games on finite graphs

The notion of observable liveness was introduced in the literature for 1-safe Petri net systems in which transitions are either observable or unobservable by a user and, among the observable ones, some are controllable, in the sense that they correspond to interactions with the user and cannot autonomously occur. An observable transition is observably live if a user can, from any reachable marking, force it to occur infinitely often by using controllable transitions. Here, we introduce a weaker version of this notion by considering the capability of the user, by means of controllable transitions, to force the considered observable transition to fire infinitely often, starting from the initial marking instead of considering each reachable marking. The main result of this paper is a method for checking weak observable liveness in state machine decomposable 1- safe nets whose transitions are observable. The introduced method is based on infinite games that are played on finite graphs. We transform the problem of weak observable liveness into a game between a system and a user, and we prove that a transition is weakly observably live if and only if the user has a winning strategy for the game.