| Revista: | Computación y sistemas |
| Base de datos: | PERIÓDICA |
| Número de sistema: | 000423349 |
| ISSN: | 1405-5546 |
| Autores: | Bárcenas, Everardo1 Benítez Guerrero, Edgard2 Benitez, Antonio3 Calleja, Jorge de la3 Medina, Ma. Auxilio3 |
| Instituciones: | 1Consejo Nacional de Ciencia y Tecnología, Ciudad de México. México 2Universidad Veracruzana, Jalapa, Veracruz. México 3Universidad Politécnica de Puebla, Puebla. México |
| Año: | 2017 |
| Periodo: | Jul-Sep |
| Volumen: | 21 |
| Número: | 3 |
| País: | México |
| Idioma: | Inglés |
| Tipo de documento: | Artículo |
| Enfoque: | Aplicado, descriptivo |
| Resumen en inglés | 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 |
| Disciplinas: | Ciencias de la computación |
| Palabras clave: | Procesamiento de datos, Planes ramificados, Lógica modal, Generador de planes, Chequeo de modelos |
| Keyword: | Data processing, Branching shaped plans, Modal logic, Plan generator, Model checking |
| Texto completo: | Texto completo (Ver HTML) Texto completo (Ver PDF) |
