SMTPlan+ is a planner for hybrid systems.

It supports all the features of PDDL+, including exogenous events and continuous processes.

SMTPlan+ provides an SMT encoding of the PDDL+ models and can handle linear domains as well as domains with nonlinear polynomial change.

PDDL+

PDDL+ is the extension of PDDL that allows modelling of mixed discrete-continuous domains, and it follows the Hybrid Automata semantics. Dealing with hybrid systems is becoming more and more an important challenge, as many real-world scenarios feature a mixture of discrete and continuous behaviours.

Compared to PDDL2.1, PDDL+ includes the following additional features, that can all be handled by SMTPlan+.

Nonlinear change Processes Events Timed Initial Literals Epsilon separation Cascading events
SMTPlan+ OK OK OK OK OK OK

SMT Encoding

The econding is based on the notion of happening, which is used to capture the change in the state at a given time point due to the effects of actions, processes, or events. Happenings describe discrete change and between happenings there is only continuous change.

Mountain View

A PDDL+ model can be described as a bounded set of happenings X:= {x1...xn } encoded as an SMT formula, such that any proof for the SMT formula represents the trace of a valid plan. The initial state is modelled in x1 , and the goal constraints are added to xn.