[Model] NonLivenessFreePetriNet

[isPANN]

Motivation

NON-LIVENESS OF FREE CHOICE PETRI NETS (GJ A12 MS3). A fundamental NP-complete problem in concurrency theory: given a free-choice Petri net, determine whether it is not live (i.e., whether some transition can never fire again from some reachable marking). Even the well-structured class of free-choice nets has intractable liveness analysis. NP membership (the harder direction) was established by Hack (1972). The NP-completeness applies to general (not necessarily bounded) free-choice nets; bounded free-choice nets have polynomial-time liveness checking (Desel & Esparza, 1995).

Associated reduction rules:

• [Rule] 3SAT to NON-LIVENESS OF FREE CHOICE PETRI NETS #920: 3SAT → NonLivenessFreePetriNet (GJ reference reduction, Jones, Landweber, Lien 1977)

Definition

Name: NonLivenessFreePetriNet
Canonical name: Non-Liveness of Free Choice Petri Nets
Reference: Garey & Johnson, Computers and Intractability, A12 MS3

Mathematical definition:

INSTANCE: A Petri net P = (S, T, F, M₀) where S is a finite set of places, T is a finite set of transitions, F ⊆ (S × T) ∪ (T × S) is the flow relation, and M₀: S → ℕ is the initial marking. P must satisfy the free-choice property: for every place s ∈ S, if |s•| > 1 (s has multiple output transitions), then •t = {s} for every t ∈ s• (each such transition has s as its only input place).

QUESTION: Is P not live? That is, does there exist a transition t ∈ T and a marking M reachable from M₀ such that t can never fire again from M?

Variables

• Count: |T| variables (one per transition)
• Per-variable domain: {0, 1} — whether the transition is eventually dead (1) or always re-enableable (0) from the current reachable marking
• Meaning: The net is "not live" if there exists any reachable marking from which at least one transition can never fire again. The brute-force solver explores the reachability graph to determine whether such a dead transition exists.

Schema (data type)

Type name: NonLivenessFreePetriNet
Variants: none (no type parameters)
Value type: Or (feasibility: is the net not live?)

Field	Type	Description
num_places	usize	Number of places |S|
num_transitions	usize	Number of transitions |T|
place_to_transition	Vec<(usize, usize)>	Arcs from places to transitions: (place_index, transition_index)
transition_to_place	Vec<(usize, usize)>	Arcs from transitions to places: (transition_index, place_index)
initial_marking	Vec<usize>	Initial marking M₀: token count for each place (length = num_places)

Getters (for overhead expressions):

• num_places() → num_places
• num_transitions() → num_transitions
• num_arcs() → place_to_transition.len() + transition_to_place.len()
• initial_token_sum() → initial_marking.iter().sum() (total tokens in M₀)

Invariant: The net must satisfy the free-choice property: for every place s with |s•| > 1, every transition t ∈ s• has •t = {s}.

Complexity

• Decision complexity: NP-complete (Jones, Landweber, Lien 1977; NP membership by Hack 1972).
• Best known exact algorithm: Explore the reachability graph. The marking space is bounded by the total token count: if M₀ has N total tokens and there are |S| places, the reachable markings are bounded by C(N + |S| - 1, |S| - 1). For a net with N total tokens, this is at most (N+1)^|S|. For each reachable marking, check if any transition is permanently dead. Worst-case: O((N+1)^num_places × num_transitions).
• declare_variants! complexity string: "(initial_token_sum + 1) ^ num_places * num_transitions"
• Note: For bounded free-choice Petri nets, liveness is decidable in polynomial time via the Rank Theorem (Desel & Esparza, 1995).

Extra Remark

Full book text (GJ A12 MS3):

INSTANCE: Petri net P = (S, T, F, M₀) satisfying the free-choice property.
QUESTION: Is P not live?

Reference: [Jones, Landweber, and Lien, 1977]. Transformation from 3-SATISFIABILITY.
Comment: The proof that this problem belongs to NP is nontrivial [Hack, 1972].

How to solve

• It can be solved by (existing) bruteforce. (Explore the reachability graph from M₀ by firing all enabled transitions. For each reachable marking, check if there exists a transition that can never be enabled again from that marking. If such a dead transition is found, the net is not live.)
• It can be solved by reducing to integer programming.
• Other: Structural analysis methods for free-choice nets (Rank Theorem, siphon/trap analysis) can solve bounded cases in polynomial time.

Example Instance

A small free-choice Petri net that is NOT live (answer: YES):

Places: s0, s1, s2  (3 places)
Transitions: t0, t1  (2 transitions)
Arcs place->transition: (s0, t0), (s1, t1)
Arcs transition->place: (t0, s1), (t0, s2), (t1, s0)
Initial marking: M₀ = [1, 0, 0]  (one token in s0)

Free-choice property check: s0 has one output transition t0 (|s0•| = 1), s1 has one output transition t1 (|s1•| = 1), s2 has no output transitions (|s2•| = 0). The free-choice property holds trivially since no place has multiple output transitions.

Execution trace:

1. M₀ = [1, 0, 0]. Only t0 is enabled (s0 has a token). Fire t0.
2. M₁ = [0, 1, 1]. Only t1 is enabled (s1 has a token). Fire t1.
3. M₂ = [1, 0, 1]. Only t0 is enabled. Fire t0.
4. M₃ = [0, 1, 2]. Only t1 is enabled. Fire t1.
5. M₄ = [1, 0, 2]. ...

The net cycles between states but tokens accumulate in s2 (a sink place). Both transitions remain fireable in this cycle, so this net appears live for t0 and t1. Let us try a net that is actually not live:

Corrected example — a net that is NOT live:

Places: s0, s1, s2, s3  (4 places)
Transitions: t0, t1, t2  (3 transitions)
Arcs place->transition: (s0, t0), (s1, t1), (s2, t2)
Arcs transition->place: (t0, s1), (t1, s2), (t2, s3)
Initial marking: M₀ = [1, 0, 0, 0]

Free-choice property check: Each place has at most one output transition, so the free-choice property holds trivially.

Execution trace:

1. M₀ = [1, 0, 0, 0]. Only t0 is enabled. Fire t0.
2. M₁ = [0, 1, 0, 0]. Only t1 is enabled. Fire t1.
3. M₂ = [0, 0, 1, 0]. Only t2 is enabled. Fire t2.
4. M₃ = [0, 0, 0, 1]. No transition is enabled — deadlock.

After reaching M₃, no transition can ever fire again. All transitions are dead. The net is not live. Answer: YES (Or(true)).

A net that IS live (answer: NO):

Places: s0, s1  (2 places)
Transitions: t0, t1  (2 transitions)
Arcs place->transition: (s0, t0), (s1, t1)
Arcs transition->place: (t0, s1), (t1, s0)
Initial marking: M₀ = [1, 0]

This is a simple cycle: t0 moves the token from s0 to s1, t1 moves it back. Both transitions can always fire again. The net is live. Answer: NO (Or(false)).

Validation

#!/usr/bin/env python3
"""Validate NonLivenessFreePetriNet examples by simulating reachability."""

def fire_transition(marking, pt_arcs, tp_arcs, t):
    """Fire transition t in the given marking. Returns new marking or None if not enabled."""
    new_marking = list(marking)
    # Check all input places have tokens and consume them
    for (p, tr) in pt_arcs:
        if tr == t:
            if new_marking[p] <= 0:
                return None
            new_marking[p] -= 1
    # Produce tokens in output places
    for (tr, p) in tp_arcs:
        if tr == t:
            new_marking[p] += 1
    return tuple(new_marking)

def is_not_live(num_places, num_transitions, pt_arcs, tp_arcs, initial_marking, max_markings=10000):
    """
    Check if the Petri net is NOT live by exploring the reachability graph.
    A net is not live if there exists a reachable marking from which some transition
    can never fire again.
    """
    from collections import deque

    initial = tuple(initial_marking)
    visited = {initial}
    queue = deque([initial])

    # Build full reachability graph
    reachability = {}  # marking -> set of successor markings
    while queue and len(visited) < max_markings:
        m = queue.popleft()
        successors = set()
        for t in range(num_transitions):
            new_m = fire_transition(list(m), pt_arcs, tp_arcs, t)
            if new_m is not None:
                successors.add(new_m)
                if new_m not in visited:
                    visited.add(new_m)
                    queue.append(new_m)
        reachability[m] = successors

    # For each reachable marking, check if some transition is dead from that marking
    for m in visited:
        for t in range(num_transitions):
            # Check if t can ever fire from m (search reachable markings from m)
            sub_visited = {m}
            sub_queue = deque([m])
            t_can_fire = False
            while sub_queue and not t_can_fire:
                current = sub_queue.popleft()
                # Can t fire at current?
                can_fire_here = True
                for (p, tr) in pt_arcs:
                    if tr == t and current[p] <= 0:
                        can_fire_here = False
                        break
                if can_fire_here:
                    t_can_fire = True
                    break
                # Explore successors
                if current in reachability:
                    for succ in reachability[current]:
                        if succ not in sub_visited:
                            sub_visited.add(succ)
                            sub_queue.append(succ)
            if not t_can_fire:
                return True  # Found a dead transition from reachable marking m
    return False


# Example 1: Not live (linear chain to deadlock)
print("=== Example 1: Linear chain (should be NOT live) ===")
result1 = is_not_live(
    num_places=4,
    num_transitions=3,
    pt_arcs=[(0, 0), (1, 1), (2, 2)],
    tp_arcs=[(0, 1), (1, 2), (2, 3)],
    initial_marking=[1, 0, 0, 0],
)
print(f"Not live: {result1}")
assert result1 == True, f"Expected True, got {result1}"

# Example 2: Live (simple cycle)
print("\n=== Example 2: Simple cycle (should be live) ===")
result2 = is_not_live(
    num_places=2,
    num_transitions=2,
    pt_arcs=[(0, 0), (1, 1)],
    tp_arcs=[(0, 1), (1, 0)],
    initial_marking=[1, 0],
)
print(f"Not live: {result2}")
assert result2 == False, f"Expected False, got {result2}"

# Verify free-choice property for both examples
def check_free_choice(num_places, pt_arcs):
    """Verify free-choice property: if |s•| > 1, then •t = {s} for all t in s•."""
    # Build s• for each place
    place_outputs = {}
    for (p, t) in pt_arcs:
        place_outputs.setdefault(p, set()).add(t)
    # Build •t for each transition
    trans_inputs = {}
    for (p, t) in pt_arcs:
        trans_inputs.setdefault(t, set()).add(p)
    # Check property
    for p, transitions in place_outputs.items():
        if len(transitions) > 1:
            for t in transitions:
                if trans_inputs.get(t, set()) != {p}:
                    return False
    return True

print("\n=== Free-choice property checks ===")
fc1 = check_free_choice(4, [(0, 0), (1, 1), (2, 2)])
print(f"Example 1 free-choice: {fc1}")
assert fc1 == True

fc2 = check_free_choice(2, [(0, 0), (1, 1)])
print(f"Example 2 free-choice: {fc2}")
assert fc2 == True

print("\nAll checks passed!")

References

• [Jones, Landweber, and Lien, 1977]: N.D. Jones, L.H. Landweber, Y.E. Lien (1977). "Complexity of Some Problems in Petri Nets." Theoretical Computer Science, 4(3), pp. 277-299.
• [Hack, 1972]: M. Hack (1972). "Analysis of Production Schemata by Petri Nets." MIT Project MAC TR-94.
• [Desel and Esparza, 1995]: J. Desel and J. Esparza (1995). Free Choice Petri Nets. Cambridge University Press.

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but no solver path identified
Non-trivial	✅ Pass	Petri net liveness is structurally distinct from all existing problems
Correctness	⚠️ Warn	References verified, but reduction algorithm is an acknowledged sketch — not the actual JLL77 construction
Well-written	❌ Fail	Missing most required Model template sections (Definition, Variables, Schema, Complexity, How to solve)

Overall: 1 passed, 2 warnings, 1 failed

---

Usefulness

The problem NonLivenessFreePetriNet does not exist in the codebase. The issue mentions a reduction from 3SAT (KSatisfiability with K=3), which would connect it to the existing reduction graph. However:

• No "How to solve" section is provided. Without at least one solver path (brute-force, ILP, etc.), reduction rules involving this problem cannot be verified via closed-loop tests. This is a warning — the problem concept is useful, but the issue needs to specify how instances will be solved.
• The motivation is present and reasonable (NP-completeness of deadlock detection in free-choice nets is a fundamental result in concurrency theory).

Non-trivial

Petri nets are a fundamentally different computational model from anything currently in the codebase. The problem involves places, transitions, arcs, markings, and the free-choice structural property — none of which map to existing graph, formula, set, or algebraic problem types. The feasibility/decision question (is the net not live?) is genuinely distinct.

Pass.

Correctness

References verified:

• Jones, Landweber, Lien (1977): "Complexity of Some Problems in Petri Nets," Theoretical Computer Science 4(3), pp. 277–299. Confirmed to exist via Semantic Scholar and ScienceDirect. The paper does address complexity of liveness problems for Petri nets.
• Hack (1972): "Analysis of Production Schemata by Petri Nets," MIT Project MAC TR-94. Confirmed to exist as a foundational Petri net reference.
• GJ entry A12 MS3: Correctly cited — Non-Liveness of Free Choice Petri Nets, with transformation from 3-Satisfiability.

Concerns:

• The reduction algorithm section is explicitly an "AI-generated summary" and the issue itself states: "The actual construction by Jones, Landweber, and Lien (1977) is more intricate to ensure the free-choice property holds globally. The above is a simplified sketch." This means the algorithm as written may not actually produce a valid free-choice Petri net, and cannot be directly implemented.
• The claim that "NP membership was established independently by Hack (1972)" could not be independently verified — Hack 1972 is about production schemata analysis, and while the GJ entry comments that "the proof that this problem belongs to NP is nontrivial [Hack, 1972]," confirming the specific theorem from the TR was not possible via web search.

Note on complexity subtlety: For bounded free-choice Petri nets, liveness is decidable in polynomial time (Barkaoui & Minoux 1992; Desel & Esparza 1995). The NP-completeness result in GJ MS3 applies to general (not necessarily bounded) free-choice nets. The issue should clarify this distinction in the Definition section.

Well-written

Missing required sections (Fail):

The issue is structured like a [Rule] issue (Source/Target, Reduction Algorithm, Size Overhead) rather than a [Model] issue. The following required Model template sections are missing entirely:

Missing Section	What is needed
Definition	Formal definition: what is a Petri net P = (S, T, F, M₀), what is the free-choice property, what does "not live" mean precisely, what is the decision question
Variables	Count, per-variable domain, semantic meaning (e.g., is each variable a transition firing sequence? a marking reachability indicator?)
Schema	Rust type name, field table with types and descriptions (places, transitions, arcs, initial marking, etc.)
Complexity	Best-known exact algorithm with citation and a concrete complexity expression (the GJ entry says NP-complete, but what is the brute-force or best exact complexity?)
How to solve	At least one solver method (brute-force reachability graph exploration? ILP encoding? direct structural analysis?)
Expected Outcome	The example gives outcomes but they are vague — no concrete witness (e.g., a specific dead transition or deadlocked marking) is provided

Example quality issues:

• The example is incomplete — it lists places and transitions but does not fully specify the arc structure needed to verify the free-choice property
• No concrete optimal/satisfying witness is given (e.g., which specific transition is dead, or which marking is a deadlock)
• The "padded to 3 literals" unsatisfiable example is only mentioned in passing, not fully worked out

Notation issues:

• The overhead table uses code names num_places and num_transitions but these are not validated against any schema since no schema is provided

Recommendations

• Restructure this issue using the [Model] template: add formal Definition, Variables, Schema, Complexity, and How to solve sections
• The reduction from 3SAT should be filed as a separate [Rule] issue once the model is implemented, OR the model issue should explicitly claim direct ILP solvability and include the reduction inline
• Consult the original JLL77 paper for the actual reduction construction rather than using the AI-generated sketch
• Consider referencing the Desel & Esparza (1995) monograph "Free Choice Petri Nets" (Cambridge University Press) for modern treatment of the structural theory
• Clarify that the NP-completeness applies to general (unbounded) free-choice nets, since bounded free-choice nets have polynomial-time liveness checking

[isPANN]

Changelog (fix-issue)

Addressed all failures from check-issue report:

1. Added missing Model template sections:

   • Definition: Formal definition of Petri net P = (S, T, F, M₀), free-choice property, and liveness question
   • Variables: |T| binary variables (one per transition), domain {0, 1}
   • Schema: Type name, value type Or, 5 fields with types and descriptions, 4 getter methods
   • Complexity: Reachability graph exploration, concrete expression "(initial_token_sum + 1) ^ num_places * num_transitions" for declare_variants!
   • How to solve: Brute-force via reachability graph exploration

2. Linked associated rule: Added reference to [Rule] 3SAT to NON-LIVENESS OF FREE CHOICE PETRI NETS #920 (3SAT → NonLivenessFreePetriNet)

3. Added getter methods: num_places(), num_transitions(), num_arcs(), initial_token_sum()

4. Replaced vague examples with concrete validated instances:

   • Example 1: Linear chain (4 places, 3 transitions) → deadlock → not live (Or(true))
   • Example 2: Simple cycle (2 places, 2 transitions) → live (Or(false))
   • Both examples verified for free-choice property compliance

5. Added Python validation script that simulates Petri net reachability and verifies both examples

6. Clarified NP-completeness scope: Applies to general (unbounded) free-choice nets; bounded free-choice nets have polynomial-time liveness checking (Desel & Esparza, 1995)

7. Removed reduction algorithm / size overhead sections (those belong in the rule issue [Rule] 3SAT to NON-LIVENESS OF FREE CHOICE PETRI NETS #920, not the model issue)

[isPANN]

Please kindly check the following items (PR #960):

• Paper (PDF): check definition, proof sketch, example figure, and reproducible pred commands
• Implementation (Optional): spot-check the source files changed in this PR for correctness

💬 Join the discussion on Zulip — feel free to ask questions or leave feedback there.