Errata to Elahi, Fadnis and Rintanen, Termination properties of transition rules for indirect effects, Proceedings of ICAPS, 2024

In Section Implementation, subsection Planning as Satisfiability, one part of the encoding is missing.

The parallel execution of regular/agent actions has to be limited so that the forced actions triggered by the two actions will not interfere.

This is achieved by formulas of the form NOT a1@t OR NOT a2@t, where a1 and a2 refer to two actions that may respectively - directly or indirectly - trigger some forced actions f1 and f2 so that these forced actions may disable or enable each other or override each other's effects.

Which actions may be triggered can be identified with the techniques used in Section Sufficient Conditions for Confluence.