Model Checking Driven Heuristic Search for Correct Programs

The Model Checking Integrated Planning System (MIPS) is a temporal least commitment heuristic search planner based on a flexible object-oriented workbench architecture. Its design clearly separates explicit and symbolic directed exploration algorithms from the set of on-line and off-line computed estimates and associated data structures. MIPS has shown distinguished performance in the last two international planning competitions. In the last event the description language was extended from pure propositional planning to include numerical state variables, action durations, and plan quality objective functions. Plans were no longer sequences of actions but time-stamped schedules. As a participant of the fully automated track of the competition, MIPS has proven to be a general system; in each track and every benchmark domain it efficiently computed plans of remarkable quality. This article introduces and analyzes the most important algorithmic novelties that were necessary to tackle the new layers of expressiveness in the benchmark problems and to achieve a high level of performance. The extensions include critical path analysis of sequentially generated plans to generate corresponding optimal parallel plans. The linear time algorithm to compute the parallel plan bypasses known NP hardness results for partial ordering by scheduling plans with respect to the set of actions and the imposed precedence relations. The efficiency of this algorithm also allows us to improve the exploration guidance: for each encountered planning state the corresponding approximate sequential plan is scheduled. One major strength of MIPS is its static analysis phase that grounds and simplifies parameterized predicates, functions and operators, that infers knowledge to minimize the state description length, and that detects domain object symmetries. The latter aspect is analyzed in detail. MIPS has been developed to serve as a complete and optimal state space planner, with admissible estimates, exploration engines and branching cuts. In the competition version, however, certain performance compromises had to be made, including floating point arithmetic, weighted heuristic search exploration according to an inadmissible estimate and parameterized optimization.

Download Full-text

Depth-First Heuristic Search for Software Model Checking

Computer and Information Science 2015 - Studies in Computational Intelligence ◽

10.1007/978-3-319-23467-0_6 ◽

2015 ◽

pp. 75-96 ◽

Cited By ~ 2

Author(s):

Jun Maeoka ◽

Yoshinori Tanabe ◽

Fuyuki Ishikawa

Keyword(s):

Model Checking ◽

Heuristic Search ◽

Software Model Checking ◽

Software Model

Download Full-text

Conformant planning via symbolic model checking and heuristic search

Artificial Intelligence ◽

10.1016/j.artint.2004.05.003 ◽

2004 ◽

Vol 159 (1-2) ◽

pp. 127-206 ◽

Cited By ~ 39

Author(s):

A. Cimatti ◽

M. Roveri ◽

P. Bertoli

Keyword(s):

Model Checking ◽

Heuristic Search ◽

Symbolic Model Checking ◽

Symbolic Model ◽

Conformant Planning

Download Full-text

Plan Existence Verification as Symbolic Model Checking

10.5753/eniac.2018.4409 ◽

2018 ◽

Author(s):

Macilio da Silva Ferreira ◽

Maria Viviane Menezes ◽

Leliane Nunes De Barros

Keyword(s):

Model Checking ◽

Heuristic Search ◽

Symbolic Model Checking ◽

State Transitions ◽

Benchmark Problems ◽

Description Language ◽

Symbolic Model ◽

Domain Description ◽

International Planning ◽

First Time

Automated Planning is the subarea of AI concerned with the generation of a plan of actions for an agent to achieve its goals. State-of-the-art planning algorithms are based on heuristic search. However, the inexistence of a plan can be a challenge for such planners, since they are not always able to discern the difficulty of finding a solution from its inexistence. The problem of plan existence verification, called planex, is computationally hard. Thus, in 2016, the planning community held for the first time the Unsolvability International Planning Competition (UIPC), which aims to evaluate algorithms on the task of verifying plan existence. The aim of this paper is to propose a new algorithm to solve the planex problem that is based on symbolic model checking approach. The proposed algorithm differs from others based on model checking in two points: (i) it is able to reason about the actions represented in PDDL (Planning Domain Description Language) and; (ii) it is based on the α-CTL logic, whose semantics takes into account the actions responsable for the state transitions. We also evaluate the proposed alorithm over the UIPC planning benchmark problems.

Download Full-text