Looking for winning strategies in two-player games on Petri nets with partial observability

TL;DR

This paper introduces a game-theoretic framework on Petri nets with partial observability, aiming to determine if a user can guarantee reaching a goal despite limited information and uncertain observations.

Contribution

It defines a new game model on Petri nets with partial observability and proposes a method to decide the existence of winning strategies under these conditions.

Findings

A formal model of games on Petri nets with partial observability.

A method to determine if a user has a winning strategy.

Analysis of the impact of observation stability on strategy existence.

Abstract

We define a game on 1-safe Petri nets, where a user plays against an environment in order to reach a goal on the system. The goal is expressed through an LTL-X formula, and represents a behaviour of the system that the user needs to guarantee. The user can try to reach his goal by controlling a subset of transitions, and by observing a subset of local states. Although we do not put any requirement on the local states observable by the user, we assume that he cannot be sure to observe them in the exact moment in which they become marked. For this reason, we define a notion of stability of the observation. We propose a method to determine whether the user has a winning strategy, i.e. if he can win every play by taking some decisions based on the information available for him.