Branching Path Planning with Modal Logics

Authors

  • Everardo Barcenas CONACYT
  • Edgard Benitez-Guerrero
  • Antonio Benitez
  • Jorge de la Calleja
  • Ma. Auxilio Medina

DOI:

https://doi.org/10.13053/cys-21-3-2444

Keywords:

Path planning, temporal logics, modal logics, model checking.

Abstract

Path planning concerns about finding a route for an agent, such that this agent move along the route from an initial to a final goal. Some additional constraints may also have to be satisfied for the agent, such as avoiding obstacles or collisions. Path planning has been recently studied in the context of linear temporal logic with great success. Expressive constraint specifications involving temporal ordering can be succinctly expressed by logic formulas, whereas environments are abstracted as transition systems. The plan is obtained by counterexample generation in a model checking tool: finding a path, if any, such that a given formula (constraints) satisfies a given model (agent environment). Due to the expressive power of linear temporal logic, only linear planning has mostly been considered so far, that is, plans corresponding to tasks to be performed in a linear successive order. In this work, we study branching shaped (tree) plans in the context of the μ-calculus, an expressive modal logic which subsumes many program logics such as LTL, PDL and CTL. Branching plans can be succinctly expressed by logic formulas so that a team of mobile devices can concurrently satisfy the plan. In the current work, we provide a plan generator based on a model checking algorithm for the μ-calculus. We show the algorithm is sound and complete, that is, for any environment, there a satisfying plan for a given set of constraints, if and only if, the plan generator succeeds.

Author Biography

Everardo Barcenas, CONACYT

Experiencia Laboral2014  a la fecha: Investigador CONACYT2012 a 2014: Profersor-Investigador de Tiempo Completo en la Universidad Politécnica de Puebla.2012 a  2014: Coordinador de la Maestría en Sistemas y Cómputo Inteligente de la Universidad Politécnica de Puebla.2011 a 2012: Investigador asociado en el Departamento de Ciencias de la Computación de la Universidad Rice.2007 a 2010: Investigador asistente en el Instituto Nacional de Investigación en Ciencias de la Computación y Control de Francia (INRIA).Estudios:Dr. en Computación. Université de Grenoble. 2011.M. C. en Lógica Computacional: Technische Universitat Wien y Universidade Nova de Lisboa. 2007.Lic. en Computación: Universidad Autónoma de Puebla. 2005. 

Downloads

Published

2017-09-28

Issue

Vol. 21 No. 3 (2017): Thematic issue: Advances in Logic-based Methods for Intelligent Systems (J. C. Nieves, E. Hermann Haeusler, B. Lopes)

Section

Articles of the Thematic Issue

License 

Hereby I transfer exclusively to the Journal "Computación y 
Sistemas", published by the Computing Research Center (CIC-IPN),
the Copyright of the aforementioned paper. I also accept that these 
rights will not be transferred to any other publication, in any other 
format, language or other existing means of developing.
I certify that the paper has not been previously disclosed or simultaneo
usly submitted to any other publication, and that it does not contain 
material whose publication would violate the Copyright or other 
proprietary rights of any person, company or institution. I certify that 
I have the permission from the institution or company where I work or 
study to publish this work.
The representative author accepts the responsibility for the publication
of this paper on behalf of each and every one of the authors. 
This transfer is subject to the following conditions:
  • The authors retain all ownership rights (such as patent rights) of this work, except for the publishing rights transferred to the CIC, through this document.
  • Authors retain the right to publish the work in whole or in part in any book they are the authors or publishers. They can also make use of this work in conferences, courses, personal web pages, and so on.
  • Authors may include working as part of his thesis, for non-profit distribution only.