Path planning concerns about ???nding a routefor an agent, such that this agent move along theroute from an initial to a ???nal goal.Some additionalconstraints may also have to be satis???ed for theagent, such as avoiding obstacles or collisions. Pathplanning has been recently studied in the context oflinear temporal logic with great success.Expressiveconstraint speci???cations involving temporal ordering canbe succinctly expressed by logic formulas, whereasenvironments are abstracted as transition systems. Theplan is obtained by counterexample generation in amodel checking tool: ???nding a path, if any, such thata given formula (constraints) satis???es a given model(agent environment). Due to the expressive power oflinear temporal logic, only linear planning has mostlybeen considered so far, that is, plans corresponding totasks to be performed in a linear successive order. Inthis work, we study branching shaped (tree) plans inthe context of theμ-calculus, an expressive modal logicwhich subsumes many program logics such as LTL, PDLand CTL. Branching plans can be succinctly expressedby logic formulas so that a team of mobile devices canconcurrently satisfy the plan. In the current work, weprovide a plan generator based on a model checkingalgorithm for theμ-calculus. We show the algorithm issound and complete, that is, for any environment, therea satisfying plan for a given set of constraints, if and onlyif, the plan generator succeeds.
展开▼
