Temporal logics have been used in autonomous planning to represent and reason about temporal planning problems. However, such techniques have typically been restricted to either (1) representing actions, events, and goals with temporal properties or (2) planning for temporally-extended goals under restrictive assumptions. We introduce Mixed Propositional Metric Temporal Logic (MPMTL) where formulae are built over mixed binary and continuous real variables. We introduce a planner, MTP, that solves MPMTL problems and includes a SAT-solver, model checker for a polynomial fragment of MPMTL, and a forward search algorithm. We extend PDDL 2.1 with MPMTL syntax to create MPDDL and an associated parser. The empirical study shows that MTP outperforms the state-of-the-art PDDL planner SMTPlan on several domains it performed best on and MTP performs and scales on problem size well for challenging domains with rich temporal properties we create.

Temporal logics have been used in autonomous planning to represent and reason about temporal planning problems. However, such techniques have typically been restricted to either (1) representing actions, events, and goals with temporal properties or (2) planning for temporally-extended goals under restrictive assumptions. We introduce Mixed Propositional Metric Temporal Logic (MPMTL) where formulae are built over mixed binary and continuous real variables. We introduce a planner, MTP, that solves MPMTL problems and includes a SAT-solver, model checker for a polynomial fragment of MPMTL, and a forward search algorithm. We extend PDDL 2.1 with MPMTL syntax to create MPDDL and an associated parser. The empirical study shows that MTP outperforms the state-of-the-art PDDL+ planner SMTPlan+ on several domains it performed best on and MTP performs and scales on problem size well for challenging domains with rich temporal properties we create.

Temporal logics have been used in autonomous planningto represent and reason about temporal planning problems.However, such techniques have typically been restricted toeither (1) representing actions, events, and goals with temporalproperties or (2) planning for temporally-extended goalsunder restrictive conditions of classical planning. We introduceMixed Propositional Metric Temporal Logic (MPMTL),where formulae in MPMTL are built over mixed binary andcontinuous real variables. MPMTL provides a natural, flexibleformalism for representing and reasoning about temporalproblems. We analyze the complexity of MPMTL formulaesatisfiability and model checking, and identify MPMTLfragments with lower complexity. We also introduce an approachto world modeling using a timeline vector, relevant totemporal planning with continuous change (as opposed to theuse of discrete states). Our model supports retroactive actionprogression, concurrent and overlapping actions with discreteand continuous changes, and concurrent effects to the samevariable. For reasoning about this temporal planning problem,we define a progression function for actions with thenew temporal properties and a solution to this temporal task.