PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Quanyan Zhu

arXiv:2610.12779v1cs.GTcs.SYeess.SY

TL;DR

Large-scale strategic systems comprise interactions whose outcomes shape what can happen next, yet the paper identifies a need to connect local games to a structural model of resources, concurrency, and reachability. It introduces OCGPNs and develops structural and strategic analyses for general and sequential nets. The results distinguish what guards can certify from what incentives can change, and provide place-wise value computation and compositional analysis.

  • Problem

    Large-scale strategic systems need a representation that makes local games, outcome-dependent later interactions, and compositional analysis coexist with resources, concurrency, and reachability.

    Source: §1 · p. 2

  • Method

    OCGPNs attach local games to colored-net places and turn resolved-game outcomes into typed tokens that govern subsequent net transitions.

    Source: §1 · p. 2

  • Results

    For general nets, guards can certify safety while incentives only change values; for sequential nets, equilibria use continuation-augmented local games and values are computed by SCCs at additive cost in local-game sizes.

    Source: §1 · p. 4

  • Takeaways & Limitations

    The theory supports compositional analysis of large strategic systems, including maintenance and intrusion examples in which downstream games affect upstream behavior and attack scenarios can be composed with an existing campaign.

    Source: §1 · pp. 4–5

    The structural certificate method is sound but incomplete: real feasibility need not imply integer feasibility, and state-equation feasibility need not imply reachability, so a missing certificate proves nothing.

    Source: §5.3 · p. 24

Abstract

from arXiv · show

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.

1 Introduction

The paper introduces outcome-driven compositional game Petri nets (OCGPNs), where local-game outcomes become typed tokens governing later interactions. It develops structural and strategic analysis for general and sequential nets, respectively.

1 Introduction

  • OCGPNs attach local games to colored-net places and convert resolved games into typed tokens that enable, synchronize, or block later interactions.One outcome can spawn several games, and several completed games may be jointly required to enable a successor.Source: §1 · pp. 3–4
  • For general concurrent nets, incidence-matrix invariants and Farkas certificates support structural analysis, while guards can certify safety and incentive instruments cannot.The separation explains why deception can lower an attacker’s value but cannot certify an outcome unreachable.Source: §1 · p. 4
  • For sequential nets, global equilibria correspond exactly to local equilibria augmented by continuation values, with values computed by SCCs at additive cost in local-game sizes.The computation solves strongly connected components in reverse topological order.Source: §1 · p. 4
  • Successor-level pivotality characterizes when downstream games change upstream behavior, alongside dominance, myopic-consistency, and monotone-comparative-statics results.These interface-design results specify when and how downstream games can change upstream behavior.Source: §1 · p. 4
  • Place fusion supports a composition calculus that glues certificates across subnets and summarizes downstream subnets by their entry values, including in general-sum games.Further results cover loop reduction, fork–join success probabilities, independence of parallel parts, and the local cost of carrying artifacts.Source: §1 · p. 4
  • The maintenance and intrusion examples show that graded routing can reverse a myopic equilibrium, costly rework can preserve cooperation, and a new attack scenario can be composed without re-solving the campaign.The paper also identifies supporting results that specialize standard theory to place-level games, including one-shot deviation and Shapley results.Source: §1 · p. 5

2 Background and motivation

The section frames composition around the interface between games, changing incentives, and analysis of composite properties. It positions OCGPNs alongside prior approaches by combining game coupling with a Petri-net structural layer.

2.1 Motivation for composition

  • Composition must specify what one game passes to the next, how downstream games affect upstream incentives, and how properties of parts establish properties of the whole.The motivating systems include interactions whose outcomes shape later participants, resources, and possibilities.Source: §2.1 · p. 6

2.2 Three views of composed games

  • Meta-games compose by abstraction, games-in-games by cross-layer nesting, and open games by information and utility flow; OCGPNs instead use token flow on a Petri-net substrate.Games-in-games already place downstream values in upstream payoffs, but do not provide a general structural layer for concurrency, shared resources, and reachability.Source: §2.2 · pp. 6–7, Figure 2 · p. 6

2.3 Related literature

  • Petri nets provide structural analysis but lack strategic players, while Petri games ask qualitative winning-strategy questions; OCGPN players occupy games at places and use payoffs and values.The related literature also includes stochastic and dynamic games, graphical models, attack graphs, and deception models, which the paper draws together for its intrusion example.Source: §2.3 · p. 8

3 Primer: Petri nets and colored tokens

Petri nets represent systems as places, transitions, and tokens; colored nets attach data to tokens and allow guards to filter transitions.

3 Primer: Petri nets and colored tokens

  • A Petri net is a bipartite graph of places and transitions, where enabled transitions consume input tokens and produce output tokens when fired.In colored Petri nets, each token carries data called a color, and a guard is a predicate on consumed colors.Source: §3 · p. 9, Figure 3 · p. 9

4 The model

Section 4 defines OCGPNs by combining colored Petri-net structure with local games and outcome-driven token routing. It also specifies the inputs and conditions governing game instances, admissible play, and resource use.

4.1 Ingredients

  • A transition binding selects the active-instance and resource tokens consumed, while colored places and markings represent typed tokens.The binding is written as the active-instance token together with the tuple of resource tokens.Source: §4.1 · pp. 10–11
  • Each game place and binding carries a local game specifying participants, feasible actions, information, utilities, outcomes, and an outcome-probability kernel.The kernel can represent deterministic outcomes, chance moves, or noisy outcomes.Source: §4.1 · p. 11
  • Resolving a game consumes its instance and bound resources, then emits typed outcome tokens that ordinary transitions route to successor games.The emitted tokens may depend on the binding, action profile, and outcome.Source: §4.1 · p. 11, Figure 4 · p. 12

4.2 General definition

  • An OCGPN combines a guarded colored Petri net with game places, resolution outputs, admissible profiles, observations, and global specifications.Its structural, game, and solution layers are associated with incidence, local-game, and routing matrices.Source: §4.2 · p. 12, Figure 5 · p. 13
  • The modeler sets a nonempty admissibility correspondence to permit local profiles, including profiles constrained by policy or regulation.This input is distinct from the equilibrium correspondence.Source: §4.2 · p. 12
  • Well-formedness requires valid token consumption, destination types, and probability kernels; an exclusivity invariant prevents resource duplication, and overlapping instances use unique identifiers.The invariant’s initial value must not exceed the resource-place capacity.Source: §4.2 · p. 13

5 General theory: semantics, analysis, and computation

This section develops the semantics and structural and strategic analysis of OCGPNs, distinguishing general nets with concurrency from sequential nets whose values and equilibria can be analyzed place by place. It characterizes termination and downstream effects on incentives, and presents a composition calculus for combining subnet properties, equilibria, and values while addressing feedback, synchronization, parallelism, and dynamic instantiation.

5.1 Operational semantics and the incidence matrix

  • The full marking semantics is necessary when parallel activities, synchronization, or shared resources matter; a successor map alone does not capture those interactions.A resolved game can produce multiple tokens and enable concurrent routes, while routing may involve exclusive choice, forks, or scheduler-resolved conflicts.Source: §5.1 · pp. 15–16
  • The unfolded incidence matrix records each transition’s net token change, but does not alone characterize enabled transitions or reachable markings.Color-and-binding guards can remove columns during unfolding, whereas guards dependent on the rest of the marking disable columns only at particular markings; strategy and outcome probabilities determine which output fires.Source: §5.1 · p. 17

5.2 Sequential OCGPNs: local and global games

  • For sequential OCGPNs, at most one game is active and exclusive routing maps each outcome to a successor game or terminal place, summarizing downstream play through routing probabilities and target values.Distinct outcomes with the same successor are strategically equivalent for continuation purposes; the model assumes finite normal-form local games and discounting, except that discount factor 1 is allowed on acyclic place graphs.Source: §5.2 · pp. 18–19
  • A stationary profile is a global equilibrium exactly when each place’s strategy is an equilibrium of its local game augmented by the continuation values generated by that profile.Myopic local equilibria generally differ from global equilibria, coinciding only in special cases.Source: §5.2 · pp. 21–22
  • A global equilibrium exists under the sequential assumptions; in the two-player zero-sum case with common players, all global equilibria yield player 1 the same value vector.For a fixed stationary profile, policy values are uniquely determined under the discounting or acyclicity conditions.Source: §5.2 · pp. 20, 22
  • Without sequential-net assumptions, concurrency requires the full global state, and an adversarial scheduler becomes a player in a finite stochastic game; exact value computation requires an adequate Markov state.When token colors encode private types, local Bayesian equilibria generally do not ensure global consistency, which may require perfect Bayesian or sequential equilibrium.Source: §5.2 · pp. 22–23

5.3 Structural analysis: reachability, safety, and progress

  • A linear reachability equation is necessary but not sufficient: its infeasibility certifies unreachability, while a Farkas certificate is sound but incomplete.The certificate is a nonnegative weighted token count that cannot increase and can be found by linear programming; invariants also constrain reachable markings. Guards can create structural certificates, whereas incentives change values rather than reachability. In bounded nets, infinite execution entails a cycle, but Nash equilibrium alone guarantees neither deadlock freedom nor eventual completion.Source: §5.3 · pp. 23–24

5.4 Strategic analysis of a game place

  • Continuation values change a player's best replies only when the interface makes some successor pivotal; if no interface is pivotal for any player, myopic local equilibria are globally consistent.With exogenous continuation values, each action comparison has at most one discount-factor threshold; endogenous values may produce multiple switching points.Source: §5.4 · pp. 26–27

5.5 Global values and computation

  • For zero-sum sequential OCGPNs with a common player pair and discount factor below 1, the place-level Shapley operator is a contraction with a unique fixed point equal to global game values.Value iteration converges geometrically. For general-sum acyclic nets, backward induction yields a global, subgame-perfect equilibrium even when the discount factor is 1; cyclic components can be solved downstream-first by SCC decomposition, with cost additive in local game sizes, excluding construction of the unfolded net.Source: §5.5 · pp. 27–30
  • Play terminates almost surely from every game place exactly when ρ(P_σ) < 1; a cycle followed with probability one instead causes livelock and makes I − P_σ singular.The spectral-radius condition is for a fixed profile under assumption 3.Source: §5.5 · p. 31

5.6 Composition and its matrix calculus

  • Place fusion glues P-invariants when component weights agree on fused places, while composite T-invariants can arise from cancellation and must be checked on the composite net.Component T-invariants extend to the composite, but the converse need not hold.Source: §5.6 · p. 32
  • A sequential composite is at equilibrium exactly when its upstream subnet is at equilibrium after downstream equilibrium values are supplied as terminal values at its exits.The downstream subnet is summarized for upstream analysis by the values it offers at its entry places.Source: §5.6 · p. 36
  • Raising a successor’s value encourages actions that make that successor more likely, while zero pivotality means the increase cannot change the relevant action comparison.The comparison is against a fixed profile of the other players’ actions.Source: §5.6 · pp. 36–37
  • Feedback reduces a single-entry loop’s value to a fixed-point formula whose denominator 1 − R(p) captures repeated attempts, with repetition dominating as R(p) approaches 1.As R(p) approaches 1, the loop’s value reflects the livelock identified by the termination result.Source: §5.6 · p. 37
  • For independent forked branches, a join fires with probability θ₁θ₂, while exactly one stranded pass token occurs with probability θ₁(1 − θ₂) + θ₂(1 − θ₁).The branches must share no places and resolve independently under stationary profiles; each branch’s contribution to joint success is scaled by the other branch’s pass probability.Source: §5.6 · pp. 37–38
  • With no shared places, subnet equilibria compose under additively separable payoffs, separate clocks, and a scheduler that eventually fires every enabled transition; shared places can require product-state value analysis.Shared-place strategic coupling can violate assumption 3, even though structural invariants still glue.Source: §5.6 · p. 38
  • Dynamic instantiation localizes state expansion to the artifact window between production and use, rather than carrying every artifact value at every game place.The contrasting global encoding has |P_G||Θ| states; in the example, W = {p_A}, so only the asset game doubles.Source: §5.6 · p. 39
  • Place fusion composes the parts, while interface redesign can address undesirable selected equilibria and proposition 11 controls artifact-carrying costs.The passage attributes place fusion to lemma 3, interface redesign to proposition 7 and theorem 2, and artifact-cost control to proposition 11.Source: §5.6 · p. 39
  • Parts are ordered by the condensation of the place graph, with downstream solutions passed upstream as entry values.Theorem 7 supplies the entry values.Source: §5.6 · p. 39
  • Within each part, loops, joins, and independent parallel parts are solved using their respective procedures.The specified procedures are theorem 3 or proposition 8 for loops, proposition 9 for joins, and proposition 10 for independent parallel parts.Source: §5.6 · p. 39

6 Running example I: strategic maintenance

The strategic maintenance example uses a planning game to show how routing, structural safeguards, and continuation values shape later play. Graded routing can reverse myopic incentives, while binary routing cannot change the comparison against low preparation.

6.1 Model

  • The planning game is a prisoner’s dilemma: low preparation strictly dominates high preparation for each player, making (L, L) its unique myopic equilibrium.The stage payoffs are illustrative, not empirically estimated.Source: §6.1 · p. 40, Table 5 · p. 40
  • Variant B routes only (H, H) to authorization and sends every other profile to recovery, whose repair token returns play to the planning game.Execution requires both an authorization token and evidence satisfying the Safe predicate and provenance certificate guard.Source: §6.1 · p. 41, Figure 10 · p. 42

6.2 Structural analysis

  • Conservation keeps exactly one work-order token, while authorization and evidence requirements exclude execution without authorization or with invalid evidence, independently of equilibrium selection.The figure states that both admissible-equilibrium branches satisfy the invariant.Source: §6.2 · p. 42, Figure 12 · p. 43
  • The net is bounded and its rework cycle is the only cycle in the reachability graph, the relevant structure for analyzing infinite executions.The cycle count vector satisfies Cn↻ = 0 and is realized by the rework cycle.Source: §6.2 · pp. 42, 44

6.3 Strategic analysis

  • In variant B, no successor is pivotal against L, so continuation values cannot change L's best reply to L.The indicators for ready and not-ready both have zero row difference against L.Source: §6.3 · pp. 44, 46
  • At γ = 0.75, graded routing makes (H, H) the unique equilibrium instead of the stage game's unique (L, L), changing the route from recovery to verification.For γ > 1/2, (H, H) is the unique equilibrium in variant A.Source: §6.1 · p. 40, §6.3 · pp. 44–45
  • With prescribed values vA = 5, vR = 0, and γ = 1, the local augmented game has both (H, H) and (L, L) as equilibria; the cyclic global game must instead determine vR endogenously.The local calculation adds a cooperative equilibrium without removing the inefficient one, so equilibrium selection remains necessary.Source: §6.3 · p. 46

H L (a) myopic stage game

The examples show how downstream routing and continuation values can change local-game incentives, while concurrent diagnostics require explicit synchronization. The analysis also distinguishes equilibrium-dependent looping from termination.

H L (a) myopic stage game

  • The stage game’s unique equilibrium is (L, L); graded routing makes (H, H) unique, while binary routing preserves both equilibria.The variants differ in downstream structure: graded consequences can make cooperation dominant, but joint-success-only coupling can add at most a coordination equilibrium, regardless of reward size.Source: Figure 14 · p. 46, Figure 15 · p. 47, H L (a) myopic stage game · p. 47

6.4 Values and computation

  • In variant B, (L, L) is always a global equilibrium for γ ∈ (0, 1), while (H, H) is an equilibrium only under an additional condition.For (L, L), V(G_P) = γc_R/(1 − γ^2); for (H, H), V(G_P) = 2 + γv_A and V(G_R) = c_R + γ(2 + γv_A).Source: §6.4 · p. 48
  • A forgiving rework loop makes shirking cheap: with c_R = 0, V(G_R) = 5.85 and (H, H) is not an equilibrium; with c_R = -3, it is an equilibrium.In the costly case, V(G_P) = 6.5, alongside a livelock equilibrium (L, L) with V(G_P) = -14.21; under (L, L), the component routing is a permutation matrix and play livelocks.Source: §6.4 · pp. 48–49

6.5 Composition with concurrent diagnostics

  • Concurrent mechanical and cybersecurity inspections activate authorization only after a join consumes matching signed pass certificates for the same work order; a failure instead produces a repair token.If one branch passes and the other fails, the pass certificate is stranded unless a cleanup transition consumes it with the repair token; a single-path game tree cannot represent this synchronization or failure mode.Source: §6.5 · pp. 49–50

7 Running example II: an intrusion campaign

The intrusion-campaign example models attacker–defender engagements with typed tokens and analyzes strategic values, reachability, and composition. It illustrates how local structure supports incremental analysis while also exposing limits on compositionality.

7 Running example II: an intrusion campaign

  • The OCGPN campaign places a technique-level attacker–defender game at each foothold, while typed tokens represent credentials, defender telemetry, and shared SOC capacity.These interfaces represent state beyond the segment where an engagement ends, including artifacts read by later games and resources contested by concurrent campaigns.Source: §7 · p. 50, §7.1 · pp. 50–51, Figure 17 · p. 52

7.2 Strategic analysis and values

  • The asset game has the pure saddle point (Enumerate, Decoy) with attacker value V_A = 11, and the attacker reaches the asset server with probability one.Under that posture, genuine data is exfiltrated with probability 3/4.Source: §7.2 · pp. 53–54

7.3 Structural analysis of guards and deception

  • Decoys lower the attacker’s value but do not make genuine exfiltration unreachable; an egress guard deletes that transition and certifies unreachability for every equilibrium.The guard acts structurally and carries an availability cost, whereas decoys change the outcome distribution and value.Source: §7.3 · p. 54

7.4 Composition

  • Typed side-place tokens localize artifacts such as stolen credentials to the games that need them, while shared SOC capacity makes concurrent campaigns strategically interdependent.With shared capacity, the defender’s feasible actions at one game place depend on the other campaign’s marking, so values must be computed over markings.Source: §7.4 · pp. 54–55

7.5 Resolution and scale

  • Coarsening the asset game overstates the attacker’s value by 4; the error bound is 26.7, while the actual upstream error is 2.65.In the 39-segment enterprise study, the decomposed model has about 104 tree nodes versus roughly 1025 for a monolithic extensive form of an eight-stage campaign.Source: §7.5 · p. 55

7.6 Composing a newly discovered scenario

  • A phishing scenario composes with the existing campaign through one fused place and its entry value, V_L = 12.11; the incremental solve agrees with a full re-solve.The compositional solve needs only the new 2 × 2 fixed point, rather than re-solving the old campaign.Source: §7.6 · pp. 57–58
  • With decoys, the composed phishing scenario gives V_U = 5.90 rather than 7.12 without decoys, while the reported strategy mixtures barely change.The phishing route reaches the IT site with probability 0.599; its probability of ending in genuine exfiltration is 0.449 with decoys, versus 0.599 without them.Source: §7.6 · p. 58
  • The compositional-equilibrium result does not apply when the new scenario shares resources with the old campaign; the composite must then be solved over its joint state.The example’s structural guarantee is obtained by gluing invariants, and its equilibrium uses the old campaign’s entry value.Source: §7.6 · p. 58

8 Conclusion

The conclusion presents OCGPNs as a framework that separates net structure from strategic incentives while supporting compositional analysis. Its results apply under stated sequentiality and finiteness assumptions, with concurrent analysis potentially requiring a large marking-level state space.

8 Conclusion

  • OCGPNs connect local games to colored Petri-net structure through typed tokens, supporting structural certificates and continuation-value analysis of strategic behavior.Place fusion composes structural certificates across subnets and summarizes downstream subnets by their entry values.Source: §8 · p. 59
  • Continuation values can make global behavior differ from myopic play, and downstream games change upstream behavior only through successors made more or less likely by a player’s action.Binary routing based only on joint success can add a cooperative equilibrium but cannot make cooperation dominant, regardless of reward size.Source: §8 · pp. 59–60
  • Forgiving rework can weaken cooperation incentives; in variant B, cooperation survives as a global equilibrium only when rework is sufficiently costly.The conclusion notes that this effect is invisible when continuation values are prescribed locally.Source: §8 · p. 60
  • Deception changes strategic values, whereas guards can certify unreachability; the two instruments operate on different layers.The conclusion recommends designing them together rather than substituting one for the other.Source: §8 · p. 60
  • A newly discovered scenario was composed through the campaign’s entry value and matched a full re-solve; computation is additive in local game sizes.Artifacts such as stolen credentials enlarge the state only within their window.Source: §8 · p. 60
  • Equilibrium and computation results require a sequential OCGPN with finite unfolding; concurrent strategic analysis falls back to a marking-level stochastic game whose state space can be large.Local games are in normal form with complete information, the scheduler is exogenous, and the cost of building the unfolded net lies outside the stated complexity bound.Source: §8 · pp. 60–61
Loading 2610.12779v1…