{
 "id": "epa1qp8f1h",
 "slug": "partial-order-reduction",
 "title": "Partial order reduction",
 "updated": "2026-10-15",
 "topic_path": [
  {
   "id": "physical",
   "label": "Physical world and mathematics",
   "api_url": "https://www.edgepedia.org/api/v1/topics/physical"
  },
  {
   "id": "physical.math",
   "label": "Mathematics and statistics",
   "api_url": "https://www.edgepedia.org/api/v1/topics/physical.math"
  },
  {
   "id": "physical.math.discrete",
   "label": "Logic and discrete mathematics",
   "api_url": "https://www.edgepedia.org/api/v1/topics/physical.math.discrete"
  },
  {
   "id": "physical.math.discrete.discrete",
   "label": "General discrete mathematics and discrete structures",
   "api_url": "https://www.edgepedia.org/api/v1/topics/physical.math.discrete.discrete"
  }
 ],
 "geo": [
  {
   "id": "geo.nongeo.t1946.physical.math.discrete",
   "label": "Non-geographic · 1946 to 2000: Logic and discrete mathematics",
   "api_url": "https://www.edgepedia.org/api/v1/geo/geo.nongeo.t1946.physical.math.discrete",
   "path": [
    {
     "id": "geo.nongeo",
     "label": "Non-geographic",
     "api_url": "https://www.edgepedia.org/api/v1/geo/geo.nongeo"
    },
    {
     "id": "geo.nongeo.t1946",
     "label": "Non-geographic · 1946 to 2000",
     "api_url": "https://www.edgepedia.org/api/v1/geo/geo.nongeo.t1946"
    },
    {
     "id": "geo.nongeo.t1946.physical",
     "label": "Physical world and mathematics",
     "api_url": "https://www.edgepedia.org/api/v1/geo/geo.nongeo.t1946.physical"
    },
    {
     "id": "geo.nongeo.t1946.physical.math",
     "label": "Mathematics and statistics",
     "api_url": "https://www.edgepedia.org/api/v1/geo/geo.nongeo.t1946.physical.math"
    },
    {
     "id": "geo.nongeo.t1946.physical.math.discrete",
     "label": "Logic and discrete mathematics",
     "api_url": "https://www.edgepedia.org/api/v1/geo/geo.nongeo.t1946.physical.math.discrete"
    }
   ]
  }
 ],
 "excerpt": "Partial order reduction is a model checking technique that combats state explosion in concurrent systems by exploiting independence between transitions, preserving properties like LTL without the next operator.",
 "snippet": "Partial order reduction is a model checking technique that combats state explosion in concurrent systems by exploiting independence between transitions, preserving properties like LTL without the next operator.",
 "node": "physical.math.discrete.discrete",
 "markdown": "# Partial order reduction\n\nPartial order reduction (POR) is a model checking technique that shrinks the state space an explicit-state verifier must explore by exploiting independence between concurrent transitions, so that concurrent and distributed systems can be verified against temporal-logic properties without enumerating every interleaving. Under interleaving semantics the state space of a concurrent system equals the product of the state counts of its threads, the main driver of the state-explosion problem; POR groups runs that differ only in the order of independent actions and explores a single representative run for each group.<sup>[1](https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec17.pdf)</sup><sup> • </sup><sup>[2](https://www.cs.cmu.edu/~emc/15-820A/reading/partial-order.pdf)</sup>\n\n| Key fact | Detail |\n|---|---|\n| Problem addressed | Interleaving semantics makes the state space the product of per-thread state counts<sup>[1](https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec17.pdf)</sup> |\n| What is reduced | The explored graph keeps at least one interleaving per Mazurkiewicz trace; optimal POR keeps exactly one<sup>[3](https://www.lix.polytechnique.fr/~cenea/papers/vmcai23.pdf)</sup> |\n| Independence | Two transitions are independent when each stays enabled after the other executes and both orders lead to the same state<sup>[2](https://www.cs.cmu.edu/~emc/15-820A/reading/partial-order.pdf)</sup> |\n| Guarantee | A reduced graph satisfying the ample-set conditions is stutter-trace equivalent to the full one, preserving LTL without the next operator<sup>[1](https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec17.pdf)</sup> |\n| Practical reduction | Depends on process coupling; combined with state-space caching, memory needs for large protocol models fell by more than 100 times<sup>[4](https://spinroot.com/spin/Workshops/ws95/godefroid.pdf)</sup> |\n| Main variants | Stubborn sets, sleep sets, persistent sets, ample sets, source sets<sup>[5](https://users.soe.ucsc.edu/%7Ecormac/papers/popl05.pdf)</sup> |\n| Modern optimum | TruSt explores exactly one interleaving per class with linear memory<sup>[6](https://pure.mpg.de/rest/items/item_3362445_2/component/file_3362446/content)</sup> |\n\n## How it works\n\nThe formal basis is an independence relation on transitions. Two transitions α and β are independent at a state if they satisfy Enabledness (if both are enabled, each remains enabled after the other executes) and [Commutativity](https://www.edgepedia.org/commutative-property) (executing them in either order reaches the same state).<sup>[2](https://www.cs.cmu.edu/~emc/15-820A/reading/partial-order.pdf)</sup> Sequences of actions that differ only by swapping adjacent independent actions are equivalent; the equivalence classes are Mazurkiewicz traces, and POR explores at least one interleaving from each trace.<sup>[7](https://orbi.uliege.be/bitstream/2268/163844/1/GW93-final%20draft.pdf)</sup><sup> • </sup><sup>[3](https://www.lix.polytechnique.fr/~cenea/papers/vmcai23.pdf)</sup> All sequences in a trace's class lead to the same deadlocks, which is why one representative detects them all.<sup>[7](https://orbi.uliege.be/bitstream/2268/163844/1/GW93-final%20draft.pdf)</sup>\n\nThe correctness argument is stutter equivalence (paths indistinguishable when invisible steps are inserted or removed). Properties expressible in temporal logics without the next-time operator (LTL\\X, CTL\\X) cannot distinguish stuttering-equivalent paths.<sup>[8](https://users.ece.utexas.edu/~garg/dist/ASE05.pdf)</sup> For a finite, action-deterministic transition system without terminal states, if every ample set satisfies the reduction conditions, the reduced system is stutter-trace equivalent to the original, so any LTL\\X formula satisfied by the reduced system holds in the full system.<sup>[1](https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec17.pdf)</sup>\n\n## How it is done\n\nThe reduction modifies depth-first search to build the reduced graph directly, selecting at each state a subset ample(s) of the enabled transitions; building the full graph first would defeat the purpose.<sup>[9](https://www.cs.cmu.edu/~emc/15817-f08/lectures/partialorder.pdf)</sup> The selection must satisfy conditions \\( C_{0} \\) through \\( C_{3} \\) (equivalently \\( A_{1} \\) through \\( A_{4} \\)): nonemptiness when the state is not fully expanded; the dependency condition, that no transition dependent on ample(s) can execute before one from ample(s); the stutter or invisibility condition, that every selected transition is invisible, meaning it does not change the propositional variables the property observes; and the cycle-closing condition, that a transition enabled along a cycle in the reduced graph must be selected in some state on that cycle, otherwise it is deferred forever and liveness checking breaks.<sup>[2](https://www.cs.cmu.edu/~emc/15-820A/reading/partial-order.pdf)</sup><sup> • </sup><sup>[9](https://www.cs.cmu.edu/~emc/15817-f08/lectures/partialorder.pdf)</sup><sup> • </sup><sup>[1](https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec17.pdf)</sup>\n\nA practical heuristic computes ample(s) as the enabled transitions of a single process, checks the dependency condition via the dependency relation and program counters, and discards the candidate when a violation is possible.<sup>[9](https://www.cs.cmu.edu/~emc/15817-f08/lectures/partialorder.pdf)</sup> Preserving branching-time logics requires the extra condition \\( C_{4} \\), that the ample set contain a single deterministic transition, which is significantly more restrictive.<sup>[10](https://webperso.info.ucl.ac.be/~pecheur/publi/FWD_ImProviso.pdf)</sup>\n\n## Origin\n\nThe semantic foundation is Antoni W. Mazurkiewicz's trace theory (1986), whose equivalence classes of action sequences underlie all POR variants.<sup>[7](https://orbi.uliege.be/bitstream/2268/163844/1/GW93-final%20draft.pdf)</sup> Patrice Godefroid reported a verification method describing system behavior in terms of Mazurkiewicz traces rather than interleavings, with \"trace automata\" that generate only one linearization per partial order, in a 1991 DIMACS paper<sup>[11](https://doi.org/10.1090/dimacs/003/21)</sup>; the same method appeared in the CAV 1990 proceedings.<sup>[12](https://link.springer.com/chapter/10.1007/BFb0023731)</sup> Antti Valmari's stubborn set method appeared in his 1991 paper \"A stubborn attack on state explosion\" in the DIMACS series.<sup>[13](https://doi.org/10.1090/dimacs/003/04)</sup> Patrice Godefroid and [Pierre Wolper](https://www.edgepedia.org/pierre-wolper)'s sleep-set paper followed in Formal Methods in System Design in 1993<sup>[14](https://doi.org/10.1007/bf01383879)</sup>, and its authors state that their simplification is close to adapting Valmari's stubborn set method to deadlock detection for Petri nets.<sup>[7](https://orbi.uliege.be/bitstream/2268/163844/1/GW93-final%20draft.pdf)</sup> Dynamic partial-order reduction for software was reported by Cormac Flanagan and Patrice Godefroid in 2005 in ACM SIGPLAN Notices<sup>[15](https://doi.org/10.1145/1047659.1040315)</sup>, and the first provably optimal DPOR algorithm by Parosh Abdulla and colleagues in 2014, also in ACM SIGPLAN Notices.<sup>[16](https://doi.org/10.1145/2578855.2535845)</sup>\n\n## Variants\n\nThe two core techniques are persistent/stubborn sets, which compute a provably sufficient subset of enabled transitions per state, and sleep sets, which exploit dependencies among currently enabled transitions plus search history; they are complementary and can be used simultaneously.<sup>[5](https://users.soe.ucsc.edu/%7Ecormac/papers/popl05.pdf)</sup> Sleep sets were the first technique to guarantee one execution per equivalence class, but they only prune transitions and cannot eliminate states when used alone.<sup>[3](https://www.lix.polytechnique.fr/~cenea/papers/vmcai23.pdf)</sup> Persistent sets provide an abstract characterization of a family of such algorithms, and are very similar to the independently introduced notion of faithful decomposition and to the ample set<sup>[17](https://patricegodefroid.github.io/public_psfiles/ieee-tse96.pdf)</sup>; an ample set is a persistent set satisfying additional conditions sufficient for LTL model checking.<sup>[5](https://users.soe.ucsc.edu/%7Ecormac/papers/popl05.pdf)</sup> Source sets, introduced for dynamic POR, are provably minimal and monotone (any superset is also a source set), properties not shared by stubborn, persistent, or ample sets; every persistent set is a source set, but some programs admit strictly smaller source sets.<sup>[3](https://www.lix.polytechnique.fr/~cenea/papers/vmcai23.pdf)</sup> For probabilistic systems, weak stubborn sets defined by conditions \\( D_{0} \\), \\( D_{1} \\), and \\( D_{2} \\) have been combined with [Markov decision process](https://www.edgepedia.org/markov-decision-process) model checking, with a reduced LTS that contains exactly the deadlocks of the original.<sup>[18](https://prismmodelchecker.org/papers/qest11por.pdf)</sup> TruSt (POPL 2022) achieved exploration-optimal DPOR with linear memory, formalized in Coq and applicable to sequential consistency and weak memory models including TSO, PSO, and RC11.<sup>[6](https://pure.mpg.de/rest/items/item_3362445_2/component/file_3362446/content)</sup> Spore (PLDI 2024) is the first stateless model checker combining symmetry reduction and DPOR soundly, completely, and optimally, achieving exponential reductions in verification time.<sup>[19](https://doi.org/10.1145/3656449)</sup> Stateful source-set algorithms combining static and dynamic computation (S-POR and variants, VMCAI 2023) beat the optimal source-set algorithm in practice, whose computation overhead subsumes its gains.<sup>[3](https://www.lix.polytechnique.fr/~cenea/papers/vmcai23.pdf)</sup>\n\n## Applications\n\nPOR is implemented in widely used explicit-state model checkers. The ULg Partial-Order Package for SPIN (versions from 1992 to 1994) implements selective search with persistent sets, sleep sets, and the proviso, in cooperation with [Gerard J. Holzmann](https://www.edgepedia.org/gerard-j-holzmann) at AT&T Bell Laboratories<sup>[4](https://spinroot.com/spin/Workshops/ws95/godefroid.pdf)</sup>; SPIN's built-in POR is ample-set based.<sup>[20](https://link.springer.com/chapter/10.1007/978-3-030-25543-5_27)</sup> The LTSmin toolset implements a language-agnostic, guard-based generalization of stubborn set theory.<sup>[21](https://spinroot.com/spin/symposia/ws13/spin2013_submission_9.pdf)</sup> An industrial VFSM validator combines persistent sets, computed from static and run-time analysis, with bit-state hashing that stores one bit per visited state<sup>[17](https://patricegodefroid.github.io/public_psfiles/ieee-tse96.pdf)</sup>, and optimal DPOR algorithms have been implemented in stateless model checkers for Erlang programs.<sup>[16](https://doi.org/10.1145/2578855.2535845)</sup>\n\nThe reduction achieved depends strongly on the system and the property. With very tight process coupling POR yields no reduction, equivalent to exhaustive search; with loose coupling it can be very impressive.<sup>[4](https://spinroot.com/spin/Workshops/ws95/godefroid.pdf)</sup> In Flanagan and Godefroid's benchmarks, when up to 11 threads access different memory locations with no hash-table conflicts, dynamic POR reduces the explored state space to a single path, while static POR suffers state explosion.<sup>[5](https://users.soe.ucsc.edu/%7Ecormac/papers/popl05.pdf)</sup> In low-level formalisms such as Petri nets or [Promela](https://www.edgepedia.org/promela), and [process algebras](https://www.edgepedia.org/process-algebra) like CSP or mCRL2, POR reduces state spaces by several orders of magnitude, but application to high-level formalisms like B and [TLA+](https://www.edgepedia.org/tla) has been disappointing: in a study of 1894 B machines, only 191 of 1121 deadlock-free machines (17%) showed any reduction, averaging 54% of the original size.<sup>[22](https://stups.hhu-hosting.de/downloads/pdf/koerner22-por-analysis.pdf)</sup>\n\n## Limitations and alternatives\n\nPOR preserves only LTL without the next operator; conditions \\( C_{0} \\) through \\( C_{3} \\) guarantee LTL\\X properties but not full LTL, because the reduction is justified by stutter equivalence.<sup>[9](https://www.cs.cmu.edu/~emc/15817-f08/lectures/partialorder.pdf)</sup><sup> • </sup><sup>[23](https://lvl.info.ucl.ac.be/uploads/Publications/CombiningPartialOrderReductionAndSymbolicModelCheckingToVerifyLTLProperties/JVM_CP_NFM_2011_REGULAR.pdf)</sup> The industrial VFSM algorithm guarantees that the reduced space contains all deadlocks, but may miss other errors such as unexpected inputs and livelocks.<sup>[17](https://patricegodefroid.github.io/public_psfiles/ieee-tse96.pdf)</sup> A 2019 study found that the standard algorithm combining on-the-fly model checking with ample-set POR is unsound; the fix transforms the property automaton into a stutter-invariant normal form, for which the corrected algorithm is sound and performs slightly better.<sup>[20](https://link.springer.com/chapter/10.1007/978-3-030-25543-5_27)</sup>\n\nSymbolic BDD-based model checking is the nearest alternative: in basic form it performs poorly on asynchronous models where interleaving drives the explosion, which is why explicit-state checkers with POR such as Spin have been preferred there, while the two approaches have also been combined for BDD-based invariant checking and LTL\\X verification.<sup>[23](https://lvl.info.ucl.ac.be/uploads/Publications/CombiningPartialOrderReductionAndSymbolicModelCheckingToVerifyLTLProperties/JVM_CP_NFM_2011_REGULAR.pdf)</sup><sup> • </sup><sup>[24](https://dl.acm.org/doi/10.1023/A:1008767206905)</sup> A polynomially close-to-optimal stateful POR algorithm cannot exist unless \\( P = NP \\), even for acyclic programs with only await instructions.<sup>[25](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.22)</sup>\n\n## References\n\n1. [Model Checking Lecture #17: Partial-Order Reduction (based on Baier & Katoen, Chapter 8)](https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec17.pdf)\n2. [State Space Reduction using Partial Order Techniques (survey by Doron Peled)](https://www.cs.cmu.edu/~emc/15-820A/reading/partial-order.pdf)\n3. [A Pragmatic Approach to Stateful Partial Order Reduction (VMCAI 2023)](https://www.lix.polytechnique.fr/~cenea/papers/vmcai23.pdf)\n4. [The ULg Partial-Order Package for SPIN](https://spinroot.com/spin/Workshops/ws95/godefroid.pdf)\n5. [Dynamic Partial-Order Reduction for Model Checking Software (Flanagan & Godefroid, POPL '05)](https://users.soe.ucsc.edu/%7Ecormac/papers/popl05.pdf)\n6. [Truly Stateless, Optimal Dynamic Partial Order Reduction (TruSt, POPL 2022)](https://pure.mpg.de/rest/items/item_3362445_2/component/file_3362446/content)\n7. [Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties (Godefroid & Wolper, 1993)](https://orbi.uliege.be/bitstream/2268/163844/1/GW93-final%20draft.pdf)\n8. [Exploiting Predicate Structure For Efficient Reachability (Garg et al., ASE 2005)](https://users.ece.utexas.edu/~garg/dist/ASE05.pdf)\n9. [Model Checking with the Partial Order Reduction (CMU lecture, Clarke/Grumberg-Peled style)](https://www.cs.cmu.edu/~emc/15817-f08/lectures/partialorder.pdf)\n10. [Efficient Symbolic Model Checking for Process Algebras (FWD-ImProviso)](https://webperso.info.ucl.ac.be/~pecheur/publi/FWD_ImProviso.pdf)\n11. [P. Godefroid (1991). Using partial orders to improve automatic verification methods. DIMACS series in discrete mathematics and theoretical computer science.](https://doi.org/10.1090/dimacs/003/21)\n12. [Using partial orders to improve automatic verification methods (Godefroid, CAV 1990)](https://link.springer.com/chapter/10.1007/BFb0023731)\n13. [A. Valmari (1991). A stubborn attack on state explosion. DIMACS series in discrete mathematics and theoretical computer science.](https://doi.org/10.1090/dimacs/003/04)\n14. [Patrice Godefroid, Pierre Wolper (1993). Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design.](https://doi.org/10.1007/bf01383879)\n15. [Cormac Flanagan, Patrice Godefroid (2005). Dynamic partial-order reduction for model checking software. ACM SIGPLAN Notices.](https://doi.org/10.1145/1047659.1040315)\n16. [Parosh Abdulla and colleagues (2014). Optimal dynamic partial order reduction. ACM SIGPLAN Notices.](https://doi.org/10.1145/2578855.2535845)\n17. [Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs (IEEE TSE 1996)](https://patricegodefroid.github.io/public_psfiles/ieee-tse96.pdf)\n18. [Partial order reduction for model checking Markov decision processes under unconditional fairness (QEST 2011, PRISM)](https://prismmodelchecker.org/papers/qest11por.pdf)\n19. [Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis (2024). SPORE: Combining Symmetry and Partial Order Reduction. Proceedings of the ACM on Programming Languages.](https://doi.org/10.1145/3656449)\n20. [What's Wrong with On-the-Fly Partial Order Reduction (SPIN 2019, Springer)](https://link.springer.com/chapter/10.1007/978-3-030-25543-5_27)\n21. [Guard-based partial-order reduction (LTSmin, SPIN 2013)](https://spinroot.com/spin/symposia/ws13/spin2013_submission_9.pdf)\n22. [POR analysis for B machines in ProB (Körner and Leuschel)](https://stups.hhu-hosting.de/downloads/pdf/koerner22-por-analysis.pdf)\n23. [Combining Partial Order Reduction and Symbolic Model Checking to Verify LTL Properties (NFM 2011)](https://lvl.info.ucl.ac.be/uploads/Publications/CombiningPartialOrderReductionAndSymbolicModelCheckingToVerifyLTLProperties/JVM_CP_NFM_2011_REGULAR.pdf)\n24. [Partial-Order Reduction in Symbolic State-Space Exploration (Alur, Brayton, Henzinger, Qadeer, Rajamani, Formal Methods in System Design, 2001)](https://dl.acm.org/doi/10.1023/A:1008767206905)\n25. [Partial-Order Reduction Is Hard (CONCUR 2025, LIPIcs)](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.22)\n\n---\n*Topic: Encyclopedia › Physical world and mathematics › Mathematics and statistics › Logic and discrete mathematics › General discrete mathematics and discrete structures*\n\n*Initially written Sep 29, 2026 · Edited: Oct 15, 2026*\n\n*Copyright 2026 EdgeChat AI, a subsidiary of Biostate AI.*\n\nLicense: Edgepedia Community License 1.0, https://www.edgepedia.org/edgepedia/license\n",
 "same_as": [
  "https://www.cs.cmu.edu/~emc/15-820A/reading/partial-order.pdf",
  "https://users.ece.utexas.edu/~garg/dist/ASE05.pdf",
  "https://www.cs.cmu.edu/~emc/15817-f08/lectures/partialorder.pdf"
 ],
 "url": "https://www.edgepedia.org/partial-order-reduction",
 "markdown_url": "https://www.edgepedia.org/partial-order-reduction.md",
 "license": {
  "name": "Edgepedia Community License 1.0",
  "url": "https://www.edgepedia.org/edgepedia/license",
  "summary": "Free with credit, commercial use included. AI training is open to everyone. For other uses, organizations over USD 100M in revenue or 100M monthly users license separately.",
  "spdx": "LicenseRef-Edgepedia-Community-1.0"
 },
 "credit": "\"Partial order reduction\", Edgepedia (EdgeChat), https://www.edgepedia.org/partial-order-reduction. Edgepedia Community License 1.0.",
 "credit_md": "\"[Partial order reduction](https://www.edgepedia.org/partial-order-reduction)\", Edgepedia (EdgeChat), [https://www.edgepedia.org/partial-order-reduction](https://www.edgepedia.org/partial-order-reduction). [Edgepedia Community License 1.0](https://www.edgepedia.org/edgepedia/license).",
 "credit_html": "\"<a href=\"https://www.edgepedia.org/partial-order-reduction\">Partial order reduction</a>\", Edgepedia (EdgeChat), <a href=\"https://www.edgepedia.org/partial-order-reduction\">https://www.edgepedia.org/partial-order-reduction</a>. <a href=\"https://www.edgepedia.org/edgepedia/license\">Edgepedia Community License 1.0</a>.",
 "speakable": "Partial order reduction is a model checking technique that combats state explosion in concurrent systems by exploiting independence between transitions, preserving properties like LTL without the next operator."
}