Symbolic model checking techniques for BDD-based planning in distributed environments

Effective plan specification, solution extraction and plan execution are critical to the ability of single- and multi-agent systems to operate given the dynamism and uncertainties that exist in real-world domains. While much traditional planning research has focused on increasing the tractable search space size for fast and efficient planning, the real-world application of domain-independent planners has suffered due to a lack of corresponding advances with respect to new domain representations, replanning in dynamic and uncertain environments and metric planning. This research implements the Metric Model Checker (MMC) to extend and enhance planning capabilities by applying symbolic model-checking (SMC) techniques for planning in causally specified domains using the causal language, C. SMC is a formal verification technique for propositional satisfiability used to test semantic properties (e.g. Computational Tree Logic) of Boolean domains. C is an action language based on a theory of causal explanation of action effects that supports action preconditions, indirect effects, non-determinism and non-inertial fluents. MMC provides five main capabilities: (i)  new domain descriptions—MMC translates and compiles C domain descriptions into a format that supports the application of model checking toolkits; (ii) extended-goal representations —MMC supports incremental plan generation for multiple, simultaneous temporally-extended goals; (iii) replanning—MMC uses BDD representations of generated plan search information to provide intelligent replanning and learning during plan execution in a manner that supports the responsive capabilities of recurrent replanning while providing the goal achievement guarantees gained from precursor methodologies, and (iv) metric planning—MMC integrates a linear programming toolkit with its Boolean model-checking algorithms to provide support for plan generation in certain metric (integer-valued) domains while mitigating the state explosion problem; and (v) distributed operation—MMC is implemented in a CORBA distributed environment that allows it to be rapidly integrated with existing agent-based systems and supports interaction with external environmental simulators.