TLDR
- A state can record ignorance. K treats a fluent as known true, known false or unknown, instead of forcing every state to be a complete possible world.
- Rules describe knowledge transitions. Causation, executability, inertia, defaults, integrity constraints and concurrency are given a stable-model-style semantics.
- Optimistic means one successful path. It needs some legal initial state and trajectory that reaches the goal; uncertainty can make that witness fragile.
- Secure means every path succeeds. The same action sequence must remain executable and achieve the goal for every legal initial state and every legal outcome.
- Representation changes the burden. A compact knowledge-state encoding can remove artificial branching, but secure planning still ranges from polynomial-hierarchy levels to NEXPTIME.
Plan over information, not an imaginary complete world
Classical planning often describes a world by assigning every relevant fluent either true or false. K permits a third condition: neither a fluent nor its explicit negation is known. That absence is not a hidden value smuggled into the state; it is the planner’s declared ignorance.
The paper begins from a practical fact. Agents frequently act without a complete view. A robot may not know whether a door is open, may lack a usable sensor, or may know only that one of several packages is dangerous. Treating every unknown as a family of fully specified worlds is legitimate, but it can multiply states and obscure which distinctions matter to the decision. Eiter and colleagues ask whether the description can instead evolve at the level of knowledge itself.
A K state is a consistent set of fluent literals. If open appears, the door is known open. If its strong negation appears, it is known closed. If neither appears, its status is unknown. Complete world states are still available: the modeller can require or generate one polarity for every fluent. Knowledge states are therefore not a rejection of ordinary planning but a generalisation that leaves some coordinates deliberately unresolved.
This shift changes what a transition means. An action can establish knowledge, preserve a known literal by inertia, withdraw the conditions that supported a conclusion, or leave a fluent open. Default negation can ask whether something is not known, while strong negation asserts the opposite value. Those two forms must not be conflated. “Not known open” does not entail “known closed”.
The language is declarative. Static background facts, typed action and fluent declarations, causal rules and executability conditions jointly determine legal transitions. The point is not merely a friendly syntax. The authors define a model-theoretic semantics analogous to answer-set semantics, then analyse the exact computational cost of optimistic planning, checking security and finding secure plans.
Worked example 1 · the unopened door
A robot whose state contains neither open nor ¬open does not possess a peculiar third physical door. It has incomplete information about an ordinary door. A rule may permit checking only while both literals are absent; after checking, alternative transitions can establish one or the other.
Causal probe 1 · why not silently choose false?
A closed-world assumption is a modelling choice, not a law of action. If every omitted fluent became false, ignorance would masquerade as evidence. K lets the modeller use a default where warranted, totalise a fluent when complete cases are required, or preserve the unknown condition when neither is justified.
Static types frame a dynamic rule language
A K planning domain separates an unchanging Datalog background from action and fluent declarations and from rules governing change. A query then supplies a ground goal and an exact plan length.
The vocabulary begins with disjoint names for actions, fluents and types, plus constants and variables. The background programme defines static relations: which objects are blocks, which locations exist, which package identifiers belong to the instance. Because this programme is normal, stratified Datalog, it has a unique answer set. That answer set determines which substitutions satisfy type declarations and hence which ground actions and fluents are legal.
A declaration such as move(B,L) requires block(B), location(L) is more than documentation. It restricts grounding to objects authorised by the background knowledge. Typed instantiation replaces variables with constants and discards rule instances whose dynamic atoms do not agree with those declarations. Safety additionally requires variables in default-negated type literals to occur in a non-default-negated type literal.
The core rule has a head, an optional condition about the current state, and an optional condition about the previous state and selected actions: caused f if B after A. With no “after” part it is static and constrains each state. With an “after” part it is dynamic. An initial-state constraint is a static rule restricted to the beginning. A head of false expresses an integrity violation.
Executability is permission by support: each selected action needs at least one satisfied executability condition. Several conditions provide alternatives. K also supplies convenient macros. inertial carries a literal forward unless its complement is established; default derives a literal unless its complement is known; total generates either polarity when neither is forced; forbidden abbreviates a false-headed rule; and noConcurrency forbids distinct actions in one step.
Worked example 2 · typed movement
If the background contains block(a) and location(table), the declaration licenses move(a,table). A constant never shown to be a block does not acquire a move instance merely because its name appears elsewhere. Type knowledge bounds the dynamic language before planning begins.
Causal probe 2 · why separate the background?
Static classification should not be recomputed as if actions could change it. Its unique model fixes the legal grounding. The transition semantics can then concentrate on dynamic literals while still consulting static facts in rule bodies.
A rule can inspect before and after
The split between an “after” body and an “if” body is the hinge of K. The former consults the previous state and executed actions; the latter constrains or supports the resulting state.
Read caused f if B after A from right to left. Suppose the previous knowledge state and chosen action set satisfy A. A candidate successor is then examined for B. If both sides hold, f must belong to that successor. This lets a rule express direct action effects, indirect effects and state constraints in a single grammatical form.
For block movement, caused on(B,L) after move(B,L) puts the block at its target. Another rule derives explicit negation for its old, distinct location. The macro inertial on(B,L) expands into a rule that copies on from the previous state when the successor does not establish its complement. The familiar frame burden is therefore handled by a compact non-monotonic pattern rather than a list of unaffected facts for each action.
Static rules have no previous-state part. In blocksworld, occupied(B) can be caused by some block being on B. Because the rule participates in every successor closure, an indirect consequence changes whenever its support changes. It need not be named as a direct effect of every move.
Action sets may contain several actions. Executability can itself depend on co-selected actions, and causal rules can rule out incompatible combinations. The convenience macro noConcurrency forces at most one action per step, but parallel execution is the default. Plan length therefore counts sets of concurrent actions, not necessarily primitive actions.
Worked example 3 · Sussman’s interleaving
For the three-block instance, K obtains the sequential plan move c to the table, move b onto a, then move c onto b. The first step temporarily disturbs one relation so the second becomes executable; the third completes the tower. A deterministic domain with one legal initial state makes this optimistic plan secure as well.
Causal probe 3 · why is inertia default-shaped?
Persistence holds unless contrary evidence is produced. If it were an unconditional positive rule, a fluent and its explicit negation could both be forced after an action. Default negation lets the new effect defeat the persistence rule while preserving the old literal in ordinary cases.
Reduce defaults, then demand the smallest supported state
K gives default negation its intended non-monotonic force in two stages. A candidate transition determines a positive reduct; legality then asks whether the successor is a minimal consistent state satisfying the surviving rules.
For a positive domain: one without default negation: a legal initial state is the smallest set closed under applicable initial and static rules. An action set is executable when every selected action has a satisfied executability condition. A transition is legal when the successor is a minimal consistent set satisfying every applicable causal rule. A false-headed applicable rule rejects the candidate.
General domains are evaluated relative to a proposed transition ⟨s,A,s′⟩. Rules whose default-negated conditions are contradicted by the relevant prior or successor information are deleted. The remaining occurrences of not L are erased. What remains is positive. This is the planning analogue of the Gelfond–Lifschitz reduct.
The candidate does not become legal merely because it satisfies the rules. Minimality prevents unsupported literals from appearing gratuitously. If nothing causes a fluent, and no surviving inertia or totality rule supports it, the fluent is absent. Strong negation is an ordinary explicit literal subject to consistency; default negation is a test used in constructing the reduct.
This self-referential check is what makes defaults useful and costly. The successor can determine which rules survive, while surviving rules determine whether that successor is minimally justified. In positive fragments the closure is more direct. In general fragments the answer-set character of the semantics can make even the existence of a legal successor computationally non-trivial.
Worked example 4 · default closed
The macro default ¬open derives known closure when open is not in the candidate state. If another rule establishes open, the default’s reduct condition fails and the closure conclusion loses support. This is defeasible belief, not an immutable physical effect.
Causal probe 4 · why insist on minimality?
Closure alone would allow a candidate to contain arbitrary knowledge unrelated to any premise. Minimality enforces a supported-state discipline: literals enter because the positive reduct requires them, not because adding them happens to preserve satisfaction.
A witness path is optimistic; a branch-proof plan is secure
The paper’s central planning distinction is quantificational. An optimistic plan needs one goal-reaching trajectory. A secure plan must survive every legal beginning and every legal continuation, never becoming stuck and always ending at the goal.
A trajectory is a sequence of legal transitions beginning in a legal initial state. An action-set sequence of the requested length is optimistic when at least one such trajectory establishes every positive goal literal and omits every default-negated goal literal. This is the familiar existential reading of planning.
In a domain with incomplete beginnings or non-deterministic effects, one successful trajectory is not a guarantee. The same plan could begin in another legal state where its next action is inapplicable, or an action could have another legal successor that misses the goal. The adjective “optimistic” marks that credulous dependence on a favourable path.
Security adds two obligations over every trajectory prefix. If the prefix has reached the plan’s length, its final state must establish the goal. If it is shorter, the next prescribed action set must have at least one legal successor, so execution cannot get stuck. Because every legal successor produces a trajectory to be checked, the overall condition covers all non-deterministic outcomes.
A secure plan must first be optimistic. The authors’ definition also requires at least one legal initial state indirectly through that premise; an inconsistent domain cannot make security vacuously true. Plans contain sets of simultaneous actions, although a sequential plan restricts each set to at most one action.
Worked example 5 · a two-step shortcut
With block d in an unknown initial location, moving c onto d and then a onto c works if d already rests on b. It is an optimistic two-step plan. It fails from other legal initial layouts, so a secure four-step plan first moves d to the table and then deliberately constructs the required stack.
Causal probe 5 · why test every prefix?
Final-state testing misses plans that cannot complete. If the prescribed second action has no legal successor after one branch of the first action, that branch never supplies a final state to inspect. Prefix executability closes this loophole.
Totalisation generates cases; constraints keep only legal ones
K can reproduce possible-world planning when a problem requires it. The total macro branches an unresolved fluent into positive and negative alternatives, while initial constraints remove impossible completions.
Consider a fourth block d whose exact location is unknown, though it is known not to be on c. To enumerate complete arrangements, the modeller totalises the relation on. Candidate states choose a polarity for each relevant ground instance. Integrity rules then demand a unique location per block, at most one block atop any block, and support chains reaching the table.
Totalisation is not passive ignorance. It expands alternatives. In answer-set terms, the paired rules derive the positive literal when its complement is not derived and vice versa. If neither is otherwise forced, distinct legal states arise. These legal starts are precisely what a secure plan must cover.
The paper’s secure four-step block plan first moves d to the table, then onto b, then moves c onto d and a onto c. The first action deliberately normalises the uncertainty: regardless of d’s legal initial location, the remainder begins from a known arrangement. The shorter optimistic plan exploits just the favourable completion where d is already on b.
Initial constraints can be economical when actions preserve them. The support conditions need only police the beginning if sequential moves maintain them. This is more than a notational convenience: preventing invalid starts before search can reduce the candidate space, provided the preservation argument is sound.
Worked example 6 · total is a controlled split
For a Boolean fluent f with no other support, total f yields one candidate with f and another with ¬f. Adding a constraint forbidding ¬f removes the second. Omitting total leaves f unknown rather than producing either completion.
Causal probe 6 · why not totalise everything?
Every unnecessary split enlarges the state family and can turn a compact knowledge problem into a combinatorial possible-world problem. Totalisation is appropriate when the plan must be validated against those alternatives, not simply because a fluent has a physical value outside the model.
The same uncertainty can be many worlds or one state of ignorance
The bomb-in-the-toilet family supplies the paper’s clearest representational comparison. A world-state encoding guesses which package is armed. A knowledge-state encoding records only which packages have been proved disarmed.
In the possible-world version BT(p), total armed(P) creates alternatives and constraints require exactly one armed package. A dunk action explicitly negates the armed fluent for its package. The derived fluent unsafe holds while some package is armed. A secure sequential plan must dunk every package because any one could contain the bomb.
The knowledge-state version begins with neither armed(P) nor its negation known. Dunking P establishes ¬armed(P), and that negative knowledge is inertial. The unsafe condition becomes epistemic: unsafe is caused when some package is not known disarmed. Only one initial knowledge state is needed. Because the transition is deterministic, optimistic and secure plans coincide, and the plan still dunks every package.
Both encodings support the intended sequence, but they organise uncertainty differently. The world version represents p alternative initial states and needs universal security to certify all of them. The knowledge version folds them into one partial state and places the burden in the goal condition. The authors argue that the latter can avoid artificial complexity for this easy family.
This is not a universal theorem that knowledge-state encodings are always faster or safer. The abstraction must preserve distinctions relevant to action choice and goal truth. If which package is armed affected another action, erasing the distinction could be unsound. The paper explicitly describes security as relative to the knowledge-state model and its defaults.
Worked example 7 · three packages
The world encoding begins with three legal worlds: bomb in 1, 2 or 3. The plan ⟨dunk 1, dunk 2, dunk 3⟩ succeeds in all three. Its one-action prefix is optimistic because one world is made safe, but not secure. In the knowledge encoding there is one initial state; that prefix still leaves packages not known disarmed, so it is not even optimistic.
Causal probe 7 · where did the universal requirement go?
It was not wished away. The knowledge encoding internalises the relevant uncertainty in the condition “every package is known disarmed”. With one deterministic trajectory, satisfying that stronger epistemic goal supplies the guarantee that world branching supplied externally.
Knowledge-state laboratory
Choose a package count, encoding and plan. The laboratory exhausts every legal world for the possible-world version and executes the single partial state for the knowledge version. Its tests encode the paper’s BT(p) contrast rather than calling an external solver.
The visual trace makes the quantifiers concrete. Under possible worlds, optimism asks whether at least one branch ends safe and security asks whether every branch does. Under the knowledge encoding, there is one deterministic branch; safety requires that every package has acquired explicit negative knowledge. An abbreviated plan therefore behaves differently at the optimistic gate even though neither encoding certifies it as secure.
An uncertain effect may branch worlds: or deliberately erase knowledge
When dunking may clog a toilet, the world-state encoding totalises the result. The knowledge-state encoding can instead stop both positive and negative inertia, leaving the clog status unknown until another rule resolves it.
The certain-clogging variant adds an inertial clogged fluent and a flush action. Dunking causes clogging, so sequentially handling p packages requires alternating dunk and flush, except after the final dunk. A minimal secure plan has 2p−1 actions. With t toilets and safe concurrency, up to t packages can be processed together.
For uncertain clogging in a possible-world encoding, total clogged after dunk(P) produces both outcomes. A secure plan cannot assume the favourable one; it must remain viable after either. The same action selection may therefore fan into several legal transitions from one state.
In a knowledge-state encoding, the paper introduces conditional inertia. A temporary fluent records that a dunk occurred. Inertia for both clogged and ¬clogged applies only when no dunk occurred. Consequently, after a dunk neither polarity is carried forward. The successor represents loss of knowledge about clog status rather than two complete successors.
This technique shows the expressiveness of transitions between partial states. It also exposes a modelling hazard. Forgetting the status is adequate only if future rules and goals interpret that ignorance correctly. A physical action is not rendered deterministic merely by refusing to represent its outcome; determinism here belongs to the formal knowledge-transition system.
Worked example 8 · dunk, then decide whether to flush
After an uncertain dunk, a world-state planner has a clogged branch and an unclogged branch. A fixed secure plan may flush next because flush is always executable and establishes known unclogged status. A knowledge-state transition can move to “clog status unknown”, from which the same conservative flush restores usable knowledge.
Causal probe 8 · does forgetting solve uncertainty?
No. It changes the representation of uncertainty. Any later action whose safety depends on actual clogging needs a rule justified at the knowledge level. A compact state is valuable when its semantics preserve the decisions under study, not merely because it has fewer nodes.
Three questions occupy different computational levels
The paper studies propositional optimistic-plan existence, security checking for a supplied optimistic plan, and secure-plan existence. It crosses those questions with fixed versus arbitrary horizon and general versus proper domains.
A proper domain is one where deciding whether a state and action set have some legal successor is polynomial. A plain domain is a recognisable syntactic subclass: it has no background programme, restricts executability, avoids default negation in postconditions and forces exactly one action in each transition. Plain domains are proper, deterministic and sequential, yet many lower bounds already hold for them.
For a fixed plan length with parallel action sets, optimistic planning is NP-complete in both general and proper domains. Security checking is ΠP₂-complete in general and co-NP-complete when successor existence is polynomial. Secure-plan existence is ΣP₃-complete in general and ΣP₂-complete for proper domains.
With arbitrary binary-encoded length, optimistic planning becomes PSPACE-complete. Security checking remains ΠP₂-complete in general and co-NP-complete for proper domains because the candidate plan is already supplied. Finding a secure plan rises to NEXPTIME-complete in both. An exponentially long plan may need to be guessed and checked across exponentially many evolving states.
Restricting fixed-length plans to sequential execution lowers secure-plan existence to ΠP₂-complete in general and DP-complete for proper domains. The number of candidate sequences becomes polynomial for a constant horizon, allowing exhaustive candidate handling, but domain consistency and universal security remain. These are exact classification results under the paper’s formal input conventions, not empirical runtime predictions.
Worked example 9 · why arbitrary length changes storage
An n-bit counter may require 2ⁿ−1 increments to reach all ones. If the horizon is written in binary, the plan can be exponentially longer than the input describing that horizon. Stepwise existential search fits polynomial space, but explicitly guessing a secure plan can require exponential time.
Causal probe 9 · why does properness help checking security?
To refute security, one may guess a bad trajectory. In a general domain, proving that the next step has no legal successor itself invokes an answer-set existence test. Properness makes successor existence polynomial, removing that inner oracle and lowering ΠP₂ to co-NP.
| Propositional problem | Fixed length, general | Fixed length, proper | Arbitrary length, general | Arbitrary length, proper |
|---|---|---|---|---|
| Optimistic plan exists | NP-complete | NP-complete | PSPACE-complete | PSPACE-complete |
| Given optimistic plan is secure | ΠP₂-complete | co-NP-complete | ΠP₂-complete | co-NP-complete |
| Secure plan exists, parallel allowed | ΣP₃-complete | ΣP₂-complete | NEXPTIME-complete | NEXPTIME-complete |
| Secure sequential plan exists | ΠP₂-complete | DP-complete | Same arbitrary-length headline | Same arbitrary-length headline |
A semantics and complexity foundation, not a universal performance result
The paper’s durable achievement is to define K precisely, demonstrate its representational choices and classify its principal propositional decision problems. Claims about implementation are supporting context, not the centre of this primary.
K can express conventional complete-world transitions, partial knowledge states, defaults, incomplete initial descriptions, non-deterministic effects and parallel action sets. The total construct moves a model towards complete alternatives; withholding totalisation preserves partiality. This flexibility is powerful precisely because the modeller must decide which semantics matches the task.
The bomb examples show how a knowledge-state formulation can avoid unnecessary branching, and the authors report faster prototype behaviour for those encodings in companion work. That result is family- and implementation-specific. It does not establish that every partial-state model dominates every possible-world model or that fewer formal states always mean less total computation.
The complexity map places limits on single-shot translations. Fixed-length optimistic planning fits NP expressiveness. Some fixed secure problems require higher polynomial-hierarchy levels, while arbitrary secure planning is NEXPTIME-complete and cannot be polynomially compiled into a PSPACE-limited formalism unless established class separations collapse. Candidate generation followed by security checking remains a possible multi-stage design.
The 2001 research report identifies open work on efficient secure planning, optimal plan costs and sensing constructs. The cover’s later copyright stamp and the later ACM DOI should not be used to rewrite the report’s historical date. Likewise, terminology has evolved: “secure” here is the paper’s formal conformant/fail-safe notion, not modern software security.
Evidence boundary
The companion follows arXiv:cs/0112006v1, a 52-page December 2001 INFSYS research report. The corresponding journal record appeared later under DOI 10.1145/976706.976708. Complexity claims apply to the stated propositional decision problems, domain classes, horizon encoding and concurrency conditions. The browser laboratory reconstructs BT(p); it is not DLVK and makes no timing comparison.
Worked example 10 · irrelevant colour
If toilets have colours and a paint action, colour need not be totalised for a goal concerned only with disarming packages: provided colour neither affects executability nor contributes causally to safety. Leaving it open focuses the model. If a later rule makes red toilets uncloggable, colour becomes relevant and the abstraction must change.
Causal probe 10 · can defaults make a secure plan unsafe in reality?
Yes, if the default assumptions in the knowledge model fail to track the actual world conditions on which execution depends. Security is formal and model-relative. The paper treats refinement and selective totalisation as ways to test feasibility under richer knowledge, not as an automatic bridge to reality.
Twelve retrieval hooks
Scholarly and publication gates
Review A · fidelity, teaching and evidential fairness
The companion was checked against all 52 pages of arXiv:cs/0112006v1: the historical introduction; overview and three contributions; syntax, safety and typed instantiation; positive and reduct-based semantics; definitions of states, legal transitions, trajectories, optimistic plans and secure plans; all macros; deterministic and incomplete blocksworld examples; world-state and knowledge-state bomb variants; the discussion of relevance and defaults; the full complexity table; theorem statements and explanatory proofs; related work; conclusion; and appendices. The 2001 report date is distinguished from its later journal publication and cover copyright metadata.
Fidelity review passed. A missing literal is never called false without an explicit closed-world or default device. Strong and default negation remain distinct. The successor minimality requirement is retained. Optimism and security use the paper’s exact existential and universal structure, including the prefix-executability clause. Totalisation is described as branching rather than sensing, except where the authors explicitly offer implicit sensing as an interpretation. Proper and plain domains are not conflated. Every complexity classification matches Table 1 or the stated sequential-plan refinement.
Teaching review passed. Ten worked examples and ten causal probes distinguish physical uncertainty, representational uncertainty, state closure, transition legality, plan quantifiers, totalisation, modelling compression, non-determinism, complexity and relevance. The ten figures reconstruct mechanisms rather than decorate headings. The laboratory exhausts complete initial worlds and the compact knowledge state for two to four packages, making the optimistic/secure contrast independently inspectable.
Review B · language, accessibility, responsive layout and execution
The prose was reviewed for inflated novelty, anthropomorphic solver claims, vague authority, historical hindsight, empirical overreach and repetitive AI-telltale transitions. British English is consistent. Each SVG has a unique title, description, caption and source note. Labels, shapes and ordering carry meaning beyond colour. Motion is non-essential and disabled under reduced-motion preferences. The page includes a skip link, ordered headings, labelled native controls, a live result region and explicit table headers.
Responsive review covers 1440, 768 and 390 pixels. The hero, five orientation cards, prose columns, all ten figures, four-control laboratory, complexity table, memory studio and paper navigation collapse without viewport overflow; the table remains independently scrollable if needed. Executable review runs every package count, both encodings and all plan presets. Three exact regressions must pass: the knowledge encoding represents one initial state while the world encoding represents p; dunking every package is secure in both; and dunking only package one is optimistic but insecure across worlds while it is not optimistic in the compact knowledge encoding.
From checking every state to making ignorance a state
Paper 0102 used epistemic logic programming to range one reverse plan over many STRIPS starting states. Paper 0103 moves the epistemic issue inside planning itself. K lets a state record what an agent knows, does not know and accepts by default, then defines how action sets transform that information. The universal burden reappears in secure planning, where one plan must survive all legal starts and outcomes.
Paper 0104 turns to De Cat, Bogaerts, Bruynooghe, Janssens and Denecker’s IDP system. Where K designs a specialised action language with answer-set-inspired semantics, IDP treats predicate logic enriched with definitions, types and aggregates as a general modelling language supporting multiple inference tasks. The canon therefore broadens from one declarative planner to a wider knowledge-base system.
Sources and audit trail
- Eiter, T., Faber, W., Leone, N., Pfeifer, G., & Polleres, A. (2001). “A Logic Programming Approach to Knowledge-State Planning: Semantics and Complexity.” INFSYS Research Report 1843-01-11. arXiv:cs/0112006. Primary 52-page source.
- Eiter, T., Faber, W., Leone, N., Pfeifer, G., & Polleres, A. “A Logic Programming Approach to Knowledge-State Planning.” ACM Transactions on Computational Logic. doi:10.1145/976706.976708. Later journal record linked by the canon.
- Eiter, T., Faber, W., Leone, N., Pfeifer, G., & Polleres, A. (2000). “Planning under Incomplete Knowledge.” Computational Logic: CL 2000, LNCS 1861, 807–821. Preliminary conference version identified by the primary.
- Gelfond, M., & Lifschitz, V. (1991). “Classical Negation in Logic Programs and Disjunctive Databases.” New Generation Computing, 9, 365–385. Stable-model reduct foundation used by K.
- Giunchiglia, E., & Lifschitz, V. (1998). “An Action Language Based on Causal Explanation.” AAAI, 623–630. Language C, the stated starting point for K’s causal-rule syntax.
- Bylander, T. (1994). “The Computational Complexity of Propositional STRIPS Planning.” Artificial Intelligence, 69, 165–204. Baseline PSPACE result used in the complexity comparison.
- Cimatti, A., & Roveri, M. (2000). “Conformant Planning via Symbolic Model Checking.” Journal of Artificial Intelligence Research, 13, 305–338. Possible-world conformant-planning context and bomb-domain naming used by the primary.
What ships with Paper 0103
Title: When the planner acts on what it knows: Eiter et al.’s language K. Standfirst: A visual and executable reconstruction of partial knowledge states, typed causal rules, stable-model transition semantics, optimistic and secure plans, possible-world versus knowledge-state bomb encodings, conditional inertia and the paper’s complexity map. Search terms: language K, knowledge-state planning, answer set programming, conformant planning, secure plan, incomplete knowledge, nonmonotonic reasoning, DLVK. Demonstration: an exhaustive BT(p) laboratory comparing possible worlds with one compact knowledge state for two to four packages. Accessibility promise: ten titled and described SVG figures, reduced-motion support, labelled controls, keyboard operation and responsive layouts.