Skip to main content

PACTL

PACTL-XR-Sym is a planner for Fully Observable Non-Deterministic (FOND) problems. It is based on a symbolic model-checking approach that uses the temporal logic α-CTL to handle temporally extended goals. This logic allows for the specification of both a condition that must be satisfied in the final state and constraints over the states visited along the way (path goals), combined with policy quality — whether weak, strong, or strong-cyclic.

A simple reachability goal is one that specifies only a condition for the final state (the target goal), while an extended reachability goal also imposes constraints on the intermediate states visited throughout the plan (the path goal).

The symbolic implementation of PACTL-XR-Sym uses Binary Decision Diagrams (BDDs) to represent states and actions in a compact and efficient way. As a result, it can explore the state space more effectively and, in many domains, outperforms planners considered to be state of the art.

Furthermore, since PACTL-XR-Sym can handle extended reachability goals, it is possible to incorporate domain knowledge to avoid undesirable states (e.g., dead-ends) directly into the goal specification. For example, in a scenario where a cargo robot must transport objects between locations, if one of the robot’s grippers is known to be defective, the goal can specify that this gripper should be avoided. Extended goals also allow the expression of preferences along the way, such as favoring safer routes or paths with specific properties.

Publications

FAQ

What is the PACTL-XR-Sym planner and how does it differ from PACTL-XR?

PACTL-XR-Sym is a symbolic version of the PACTL-XR planner. While the algorithms in PACTL-XR were designed to reason directly over the states and transitions of the planning domain, the algorithms in PACTL-XR-Sym reason over sets of states represented by logical formulas encoded using Binary Decision Diagrams (BDDs).

Is PACTL-XR-Sym available for testing?

Not yet. However, we are currently working on refactoring and other improvements to release a new version soon. A prototype of this planner is available here.

What is the temporal logic α-CTL and how is it used in planning with PACTL-XR-Sym?

α-CTL is a branching-time temporal logic that extends CTL (Computation Tree Logic) and, unlike CTL, incorporates actions into its semantics.

For more information about this logic, see: A logic-based agent that plans for extended reachability goals.

PACTL-XR-Sym uses α-CTL to express complex goals. Our planner directly implements the logic’s semantics to synthesize a policy.

How are the problems to be solved specified for PACTL-XR-Sym?

They are specified through domain and problem descriptions formulated in PDDL (Planning Domain Definition Language), a standard language for modeling planning tasks in automated planning systems.

Authors

Viviane Bonadia dos Santos, Leliane Nunes de Barros, Maria Viviane de Menzes, Silvio do Lago Pereira