MIPS [EdelkampEdelkamp2003] uses a variety of techniques, but at the core is a model-checker based on ordered binary decision diagrams (OBDDs), which is used to generate reachable states. The planner uses a powerful technique to compress state representations in order to make the OBDDs more compact. Exhaustive search of the state space is impractical in large problems and MIPS uses a heuristic evaluation function based on relaxed plans in order to restrict the space of explored states. MIPS tackles concurrency in temporal planning by lifting partial orders from the totally ordered plans that are produced by its forward search. MIPS has also been extended to manage metric quantities, also using a relaxation heuristic to predict the behaviours of metric quantities.