Agent motion planning with pull and push moves

Proof-Carrying Code Usando Cálculo de Hoare

Tadeu ZubaranMarcus Ritt

Juliana Carpes ImperialEdward Hermann Haeusler

Agent motion planning is a common task in artificial intelligence. One of the simplest scenarios considers the delivery of boxes to storage loca- tions on a regular grid with obstacles. When the agent can only push boxes, we obtain the well-known, PSPACE-hard Sokoban puzzle [Culberson 1997]. In this paper we propose an exact solver for the scenario called Pukoban where the agent can push and pull boxes. The solver is, to the best of our knowledge, the first one proposed for Pukoban. It is based on the A* search algorithm with sev- eral problem-specific improvements. We evaluate its efficiency on 100 instances from the literature. Our algorithm is able to solve 30 instances exactly. Since programs source are usually unknown, it is necessary to besure that the code of the program behaves as expected. The ideal solutionwould be verifying the code against a specification of safety policies.However, this can take too much time. Another approach is making the codeitself prove that it is safe. The concept of proof-carrying code (PCC) is basedon this idea: a program carries a proof of its conformity with certain safetypolicies. Therefore, the same formal methods employed in formal verificationof programs can be used in this technology. Due to this fact, this work studieshow Hoare logic applied to source codes written in an imperativeprogramming language can be useful to PCC.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: