Game petri nets model strategic systems with local decision games

Game Petri Nets: Compositional Modeling and Analysis of Large-Scale Strategic Systems

Computer Science and Game Theory

Summary

Complex systems like maintenance workflows or cyber-attacks have many parts where decisions affect what happens next. The authors introduce game Petri nets, a way to break down these systems into local games linked by tokens, which track how decisions enable or block future actions. They provide mathematical tools to analyze these nets, showing how global strategies come from local decisions and how parts influence each other. This approach helps to understand and compute outcomes step-by-step for large, connected games.

What this means in practice

  • For cyber defense teams: Analyze complex cyber intrusion campaigns by composing and evaluating individual attack steps as local strategic games within a larger attack model.
  • For industrial operations managers: Model and analyze large maintenance workflows where outcomes of local decisions affect resource use and task sequencing.

A theory result. No direct application yet.

Authors

Quanyan Zhu

Abstract

Large-scale strategic systems, such as maintenance workflows, cyber campaigns, and multi-agent AI pipelines, consist of many interactions whose outcomes determine which later interactions become possible, who takes part, and with what resources. We introduce game Petri nets, formalized as outcome-driven compositional game Petri nets (OCGPNs), to model and analyze such systems. Local games are attached to places of a colored Petri net, and a game-to-token interface converts each resolved game into typed tokens that enable, synchronize, or block subsequent games. For general, concurrent nets, we give an operational semantics and a structural theory based on invariants and Farkas certificates, which shows that guards can certify unreachability whereas incentive instruments can only change values. For sequential nets, the net induces a stochastic game on its game places. We prove that global equilibria are exactly collections of equilibria of local games augmented by continuation values, characterize through successor-level pivotality when downstream games change upstream behavior, and compute values place by place via a decomposition into strongly connected components, at a cost additive in local game sizes. A composition calculus based on place fusion glues certificates across subnets and summarizes downstream subnets by their entry values. Two running examples, a maintenance workflow and an intrusion campaign derived from multi-resolution cyber-defense games, illustrate the theory, including the composition of a newly discovered attack scenario with an existing campaign.