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.
展开▼
机译：考虑到现实世界中存在的动态性和不确定性，有效的计划规范，解决方案提取和计划执行对于单代理和多代理系统的运行能力至关重要。尽管许多传统的计划研究都集中于增加可搜索的搜索空间大小以进行快速有效的计划，但由于缺乏与新领域表示，动态计划和重新计划有关的相应进展，与领域无关的计划者在现实世界中的应用受到了影响。不确定的环境和指标计划。这项研究实施度量模型检查器（MMC），以通过使用因果语言 C 在因果指定的领域中进行计划的符号模型检查（SMC）技术来扩展和增强计划功能。 SMC是用于命题可满足性的形式验证技术，用于测试布尔域的语义属性（例如计算树逻辑）。 C 是一种基于动作效果的因果解释理论的动作语言，该理论支持动作前提，间接效果，不确定性和非惯性流利性。 MMC提供五种主要功能：（i）新域描述-MMC将 C 域描述转换并编译为支持模型检查工具箱应用的格式； （ii）扩展目标表示-MMC支持为多个同时进行的时间扩展目标生成增量计划； （iii） replanning -MMC使用生成的计划搜索信息的BDD表示在计划执行期间提供智能的重新计划和学习，以支持循环重新计划的响应能力，同时提供从前体获得的目标成就保证方法和（iv）<斜体>度量标准-MMC将线性编程工具包与其布尔模型检查算法集成在一起，为某些度量（整数值）域中的计划生成提供支持，同时减轻了状态爆炸问题; （v）分布式操作-MMC在CORBA分布式环境中实现，可使其与现有的基于代理的系统快速集成，并支持与外部环境模拟器的交互。
展开▼
