在具有部分可观测性的Petri网双人博弈中寻找获胜策略

我们定义在1-安全Petri网上的一种博弈，其中用户与环境对抗以在系统上达成目标。目标通过LTL-X公式表达，并表示用户需要保证的系统行为。用户可尝试通过控制一部分变迁并观测一部分局部状态来达成其目标。尽管我们对用户可观测的局部状态不加任何要求，我们假设他无法确信在它们被标记的确切时刻观测到它们。为此，我们定义一种观测稳定性的概念。我们提出一种方法以确定用户是否具有获胜策略，即他能否基于可用信息做出某些决策来赢得每一局博弈。