Robust Multi-Robot Optimal Path Planning with Temporal Logic Constraints  Alphan Ulusoy ?   Stephen L. Smith †   Xu Chu Ding ‡   Calin Belta ?  Abstract — In this paper we present a method for automati- cally planning robust optimal paths for a group of robots that satisfy a common high level mission specification. Each robot’s motion in the environment is modeled as a weighted transition system, and the mission is given as a Linear Temporal Logic (LTL) formula over a set of propositions satisfied by the regions of the environment. In addition, an optimizing proposition must repeatedly be satisfied. The goal is to minimize the maximum time between satisfying instances of the optimizing proposition while ensuring that the LTL formula is satisfied even with uncertainty in the robots’ traveling times. We characterize a class of LTL formulas that are robust to robot timing errors, for which we generate optimal paths if no timing errors are present, and we present bounds on the deviation from the optimal values in the presence of errors. We implement and experimentally evaluate our method considering a persistent monitoring task in a road network environment.  I. I NTRODUCTION  The classic motion planning problem considers missions where a robot must reach a goal state from an initial state while   avoiding   obstacles.   Temporal   logics,   on   the   other hand, provide a powerful high-level language for specifying complex missions for groups of robots [1], [2], [3], [4], [5]. Their power lies in the wealth of tools from model checking [6], [7], which can be leveraged to generate robot paths satisfying desired mission specifications. Alternatively, if the mission cannot be satisfied, the tools can be used produce a certificate, or counter-example, which proves that the mission is not possible. However, in robotics the goal is typically to plan paths that not only complete a desired mission, but which do so in an optimal manner. In our earlier work [8] we considered Linear Temporal Logic (LTL) specifications, and a particular form of cost function, and provided a method for computing optimal robot paths for a single robot. We then extended this approach to multi-robot problems by utilizing timed automata [9]. The main difficulty in moving from a single robot to multiple robots is in synchronizing the motion of the robots, or in allowing the robots to move asynchronously. In [10], the authors propose a method for decentralized motion of multiple   robots   by   restricting   the   robots   to   take   transi- tions ( i.e. , travel along edges in the graph) synchronously.  This work was supported in part by ONR-MURI N00014-09-1051, ARO W911NF-09-1-0088, AFOSR YIP FA9550-09-1-020, NSF CNS-0834260, NSF CNS-1035588 and NSERC.  ?   Hybrid and Networked Systems Laboratory, Boston University, Boston, MA 02215 ( alphan@bu.edu ,   cbelta@bu.edu )  †   Dept. of Electrical and Computer Engineering, University of Waterloo, Waterloo ON, N2L 3G1 Canada ( stephen.smith@uwaterloo.ca )  ‡   Embedded   Systems   and   Networks,   United   Technologies   Research Center, East Hartford, CT 06108 ( dingx@utrc.utc.com )  Once every robot has completed a transition, the robots can synchronously make the next transition. While such an approach is effective for satisfying the LTL formula, it does not lend itself to optimizing the robot motion, since robots must spend extra time for synchronization. In [9] we approached this problem by describing the motion of the group of robots in the environment as a timed automaton. This description allowed us to represent the relative position between robots. Such information is necessary for optimizing the robot motion. After providing a bisimulation [11] of the infinite-dimensional timed automaton to a finite dimensional transition system we were able to apply our results from [8] to compute an optimal run. However, enabling the asynchronous motion of robots introduces issues in the robustness, and thus implementability of the multi-robot paths. Timed-automata rely heavily on the assumption that the clocks (or for robots, the speeds), are known exactly. If the clocks drift by even an infinitesimally small amount, then the reachability analysis developed for timed-automata is no longer correct [12], [13]. The intuition behind this is that if the robot speeds are not exactly equal to those used for planning, then two robots can complete tasks in a different order than was specified in the plan. This switch in the order of events may result in the violation of the global mission specification. In this paper, we address this issue by characterizing a class of LTL formulas that are robust to such timing errors. For simplicity of presentation, we assume that each robot moves among the vertices of an environment modeled as a graph. However, by using feedback controllers for facet reachability in polytopes [14] the method developed in this paper can be extended to robots with continuous dynamics traversing an environment with polytopic partitions. The characterization relies on the concept of trace-closedness of languages, which was first applied in multi-robot planning in [15]. For these languages, we can guarantee that any de- viation from the planned order of events due to uncertainties in the speeds of robots will not result in the violation of the global specification. The contribution of this paper is to present a method for generating paths for a group of robots satisfying general LTL formulas, which are robust to uncertainties in the speeds of robots, and which perform within a known bound of the optimal value. We focus on minimizing a cost function that captures the maximum time between satisfying instances of an   optimizing proposition . The cost is motivated by problems in persistent monitoring and in pickup and delivery problems. Our solution relies on using the concept of trace-closedness  arXiv:1202.1307v2 [cs.RO] 10 Jul 2012
to characterize the class of LTL formulas for which a robust solution exists. For formulas in this class, we utilize a similar method as in [9] to generate robot plans. We then propose periodic synchronization of the robots to optimize the cost function in the presence of timing errors. We provide results from an implementation on a robotic test-bed, which shows the utility of the approach in practice. The organization of the paper is as follows. In Section II, we give some preliminaries in formal methods and trace- closed languages. In Section III, we formally state the motion planning problem for a team of robots, and we present our solution in Section IV. In Section V, we present a hardware implementation for a team of robots performing persistent data gathering missions in a road network environment. Finally, in Section VI, we conclude with final remarks. II. P RELIMINARIES  For a set   Σ , we use   | Σ | ,   2 Σ ,   Σ ∗ , and   Σ ω   to denote its cardinality, power set, set of finite words, and set of infinite words, respectively. Moreover, we define   Σ ∞   = Σ ∗   ∪   Σ ω  and denote the empty string by   ∅ .  Definition II.1   ( Transition System).   A (weighted) transition system (TS) is a tuple   T   :=   ( Q T , q 0 T , δ T ,   Π T ,   L T , w T ) , where  (i)   Q T   is a finite set of states;  (ii)   q 0 T   ∈ Q T   is the initial state;  (iii)   δ T   ⊆ Q T   × Q T   is the transition relation;  (iv)   Π T   is a finite set of atomic propositions (observations);  (v)   L T   :   Q T   →   2 Π T   is a map giving the set of atomic propositions satisfied in a state;  (vi)   w T   :   δ T   →   R > 0   is a map that assigns a positive weight to each transition.  We define a run of   T   as an infinite sequence of states  r T   =   q 0 q 1   . . .   such that   q 0   =   q 0  T   ,   q k   ∈ Q T   and   ( q k , q k +1 )   ∈  δ T   for all   k   ≥   0 . A run generates an infinite word   ω T   =  L ( q 0 ) L ( q 1 )   . . .   where   L ( q k )   is the set of atomic propositions satisfied at state   q k .  Definition II.2   ( LTL Formula).   An LTL formula   φ   over the atomic propositions   Π   is defined inductively as follows:  φ   ::=   > |   α   |   φ   ∨   φ   |   φ   ∧   φ   | ¬   φ   |   X   φ   |   φ   U   φ  where   >   is a predicate true in each state of a system,   α   ∈   Π  is an atomic proposition,   ¬   (negation),   ∨   (disjunction) and  ∧   (conjunction) are standard Boolean connectives, and   X  and   U   are temporal operators.  LTL formulas are interpreted over infinite words (gener- ated by the transition system   T   from Def. II.1). Informally,  X   α   states that at the next position of a word, proposition   α   is true. The formula   α 1   U   α 2   states that there is a future position of the word when proposition   α 2   is true, and proposition   α 1  is true at least until   α 2   is true. From these temporal operators we can construct two other temporal operators: Eventually (i.e., future),   F   defined as   F   φ   :=   > U   φ , and Always (i.e., globally),   G , defined as   G   φ   :=   ¬   F   ¬   φ . The formula   G   φ  states that   φ   is true at all positions of the word; the formula  F   φ   states that   φ   eventually becomes true in the word. More expressivity can be achieved by combining the temporal and Boolean operators. We say a run   r T   satisfies   φ   if and only if the word generated by   r T   satisfies   φ .  Definition II.3   ( B  ̈ uchi Automaton).   A B ̈ uchi automaton is a tuple   B   := ( S B ,   S 0 B ,   Σ B , δ B ,   F B ) , consisting of  (i)   a finite set of states   S B ;  (ii)   a set of initial states   S 0 B   ⊆ S B ;  (iii)   an input alphabet   Σ B ;  (iv)   a non-deterministic transition relation   δ B   ⊆ S B   × Σ B   × S B ;  (v)   a set of accepting (final) states   F B   ⊆ S B .  A   run   of   B   over an input word   ω   =   ω 0 ω 1   . . .   is a sequence  r B   =   s 0 s 1   . . . , such that   s 0   ∈ S 0 B , and   ( s k , ω k , s k +1 )   ∈   δ B , for all   k   ≥   0 . A B ̈ uchi automaton   B   accepts a word over   Σ B  if and only if at least one of the corresponding runs intersects with   F B   infinitely many times. For any LTL formula   φ   over a set   Π , one can construct a B ̈ uchi automaton with input alphabet   Σ B   = 2 Π   accepting all and only words over   2 Π  that satisfy   φ .  Definition II.4   ( Prefix-Suffix Structure).   A prefix of a run is a finite path from an initial state to a state   q . A periodic suffix is an infinite run originating at the state   q   reached by the prefix, and periodically repeating a finite path, which we call the suffix cycle, originating and ending at   q , and containing no other occurrence of   q . A run is in prefix-suffix form if it consists of a prefix followed by a periodic suffix.  Definition II.5   ( Language).   The set of all the words ac- cepted by an automaton   B   is called the language recognized by the automaton and is denoted by   L B .  Definition II.6   ( Distribution).   Given a set   Σ , the collection of subsets   Σ i   ⊆   Σ ,   ∀   i   = 1 , . . . , m   is called a distribution of   Σ   if   ∪ m i =1 Σ i   = Σ .  Definition II.7   ( Projection).   For a word   ω   ∈   Σ ∞   and a subset   Σ i   ⊆   Σ ,   ω    Σ i   denotes the projection of   ω   onto   Σ i , which is obtained by removing all the symbols in   ω   that are not in   Σ i . For a language   L   ⊆   Σ ∞   and a subset   Σ i   ⊆   Σ ,  L    Σ i   denotes the projection of   L   onto   Σ i , which is the set of projections of all words in   L   onto   Σ i , i.e.,   { ω    Σ i   |   ω   ∈   L } .  Definition II.8   ( Trace-Closed Language).   Given the distri- bution   { Σ 1 , . . . ,   Σ m }   of   Σ   and the words   ω, ω ′   ∈   Σ ∞ ,   ω ′   is trace-equivalent to   ω , denoted   ω ′   ∼   ω , iff their projections onto each one of the subsets in the given distribution are equal, i.e.,   ω    Σ i   =   ω ′    Σ i   for each   i   =   1 , . . . , m . For  { Σ 1 , . . . ,   Σ m } , the trace-equivalence class of   ω   is given by  [ ω ] =   { ω ′   ∈   Σ ∞   |   ω ′    Σ i   =   ω    Σ i   ∀ i   = 1 , . . . , m } . Finally, a trace-closed language over   { Σ 1 , . . . ,   Σ m }   is a language   L  such that   [ ω ]   ⊆   L,   ∀   ω   ∈   L .  III. P ROBLEM   F ORMULATION AND   A PPROACH  In this section we introduce the multi-robot path planning problem with temporal constraints, and we motivate the need for solutions that are robust to uncertain robot speeds.
A. Environment Model and Initial Formulation  Let  E   = ( V,   → E   )   (1) be a graph, where   V   is the set of vertices and   → E   ⊆   V   ×   V  is the set of edges. In this paper,   E   is the quotient graph of a partitioned environment, where   V   is a set of labels for the regions in the partition and   → E   is the corresponding adjacency relation. For example,   V   can be a set of labels for the roads, intersections, and buildings in an urban-like environment and   → E   gives their connections (see Fig. 4). Consider a team of   m   robots moving in an environ- ment   modeled   by   E .   The   motion   capabilities   of   robot  i   ∈   { 1 , . . . , m }   are   represented   by   a   TS   T i   = ( Q i , q 0  i   , δ i ,   Π i ,   L i , w i ) , where   Q i   ⊆   V   ;   q 0  i   is the initial vertex of robot   i ;   δ i   ⊆→ E   is a relation modeling the capability of robot   i   to move among the vertices;   Π i   is the subset of propositions   Π   assigned to the environment that can be satisfied by robot   i   such that   { Π 1 , . . . ,   Π m }   is a distribution of   Π ;   L i   is a mapping from   Q i   to   2 Π i   showing how the propositions are satisfied at vertices;   w i ( q, q ′ )   captures the time for robot   i   to go from vertex   q   to   q ′ , which we assume to be an integer. In this robotic model, robot   i   travels along the edges of   T i , and spends zero time on the vertices. We assume that the robots are equipped with motion primitives which allow them to move from   q   to   q ′   for each   ( q, q ′ )   ∈   δ i . In our previous work [9] we considered the case where there is an atomic proposition   π   ∈   Π , called the   optimizing proposition , and a multi-robot task specified by an LTL formula of the form  φ   :=   φ   ∧   GF π,   (2) where   φ   can be any LTL formula over   Π , and   GF π   specifies that proposition   π   must be satisfied infinitely often. As an example, in a persistent data gathering task,   π   may be assigned to regions where data is uploaded,   i.e. ,   π   =   Upload , while   φ   can be used to specify rules (such as traffic rules) that must be obeyed at all times during the task [8]. Our goal in [9] was to plan multi-robot paths that satisfy  φ   and   minimize   the   maximum   time   between   satisfying instances of   π . In data gathering, this corresponds to min- imizing the maximum time between data uploads. To state this problem formally, we assume that each run   r i   =   q 0  i   q 1  i   . . .  of   T i   (robot   i ) starts at   t   = 0   and generates a word   ω i   =  ω 0  i   ω 1  i   . . .   and a corresponding sequence of time instances  T i   :=   t 0  i   t 1  i   . . .   such that the   k th   symbol   ω k i   =   L i ( q k i   )   is satisfied at time   t k i   . Note that, as robots spend zero time on the vertices, each   ω k i   has a unique   t k i   which is the instant when robot   i   visits the corresponding vertex. To define the behavior of the team as a whole, we consider the sequences  T i   as sets and take the union   ⋃ m i =1   T i   and order this set in ascending order to obtain   T   :=   t 0 t 1 , . . . . Then, we define  ω team   =   ω 0  team ω 1  team   . . .   to be the word generated by the team of robots where the   k th   symbol   ω k team   is the union of all propositions satisfied at time   t k . Finally, we define the infinite sequence   T π   =   T π   (1) ,   T π   (2) , . . .   where   T π   ( k )  stands for the time instance when the optimizing proposition  π   is satisfied for the   k th   time by the team. Thus, the problem is that of synthesizing individual optimal runs for a team of robots so that   ω team   satisfies   φ   and   T π   minimizes  J ( T π   ) = lim sup  k → + ∞  ( T π   ( k   + 1)   −   T π   ( k ))   .   (3) Since we consider LTL formulas containing   GF π , this optimization problem is always well-posed.  B. Robustness and Optimality in the Field  In this paper, we are interested in the implementability of our previous approach in the case where our model is not exact in the weights of transitions. Particularly, we consider the case where the actual value of   w i ( q, q ′ )   that is observed during deployment, denoted by    ̃ w i ( q, q ′ ) , is a non-deterministic quantity that lies in the interval   [(1   −  ρ i ) w i ( q, q ′ ) ,   (1+ ρ i ) w i ( q, q ′ )]   where   ρ i   is the   deviation value  of robot   i   which is assumed to be known a priori. In the following, we use the expression “ in the field ” to refer to the model with uncertain traveling times, and use   x   and    ̃ x  to denote the planned and actual values of some variable   x . The   question   becomes,   if   we   use   the   runs   generated from our previous approach in the field, will the formula   φ  still be satisfied? Given the word   ω team   that characterizes the planned run of the robotic team and the distribution  { Π 1 , . . . ,   Π m } , the   actual   word    ̃ ω team   generated by the robotic team during its infinite asynchronous run in the field will be one of the trace equivalents of   ω team ,   i.e. ,    ̃ ω team   ∈  [ ω team ]   due to the uncertainties in the traveling times of the robots. This leads to the definition of critical words.  Definition III.1   ( Critical Words).   Given the language   L B  of the B ̈ uchi automaton that corresponds to the LTL formula  φ   over   Π , and given a distribution of   Π , we define the word  ω   over   Π   to be a   critical word   if   ∃    ̃ ω   ∈   [ ω ]   such that    ̃ ω   6   ∈   L B .  Thus, we see that if the planned word is critical, then we may not satisfy the specification in the field. This can be formalized by noting that the optimal runs that satisfy (2) are always in a prefix-suffix form [16], where the suffix cycle is repeated infinitely often. Using this observation and Def. III.1 we can formally define the words that can violate the LTL formula during the deployment of the robotic team.  Proposition III.2.   If the suffix cycle of the word   ω team   is a critical word, then the correctness of the motion of the robotic team during its deployment cannot be guaranteed. Proof.   We denote the actual word generated by the robotic team in the field by    ̃ ω team   whereas   ω team   stands for the planned word. Suppose that for each robot   ρ i   =    , and in the suffix cycle we have   ω k team   and   ω ( k + τ   )  team   generated by robots   i   and   j   at positions   k   and   k   +   τ   that must not be swapped, because if they do    ̃ ω team   violates   φ . Note that we are guaranteed to find such symbols as we assume the suffix cycle to be a critical word. In the worst-case, for the symbols to swap, we must have   (1 +    ) t k   >   (1   −    ) t k + τ   . Solving for   , we get    >   ( t k + τ   − t k ) / ( t k   + t k + τ   ) . However, as the suffix is an infinite repetition of the suffix cycle,   lim k →∞ ( t k + τ   −  t k ) / ( t k   +   t k + τ   ) = 0   and   φ   is violated for any    >   0 .   
In addition, we can consider the performance of the team during deployment in terms of the value of the cost function (3) observed in the field. Using the same arguments presented in Prop. III.2 it can be easily show that, the worst-case field value of (3) will be the minimum of   (  ̃ J 1 , . . . ,    ̃ J m )   where   ̃ J i   is the maximum duration between any two successive satisfactions of   π   by robot i in the field. This effectively means that there is no benefit in executing the task with multiple robots, as at some point in the future the overall performance of the team will be limited by that of a single member.  C. Robust Problem Formulation  To characterize the field performance of the robotic team and to limit the deviation from the optimal run during deployment, we propose to use a synchronization protocol where robots can synchronize with each other only when they are at the vertices of the environment. We assume that there is an atomic proposition   Sync   ∈   Π , called the  synchronizing proposition , and we consider multi-robot tasks specified using LTL formulas of the form  φ sync   :=   φ   ∧   GF π   ∧   GF Sync ,   (4) where   φ   can be any LTL formula over   Π ,   π   is the opti- mizing proposition and   Sync   is the special synchronizing proposition that is satisfied only when all members of the robotic team occupy vertices at the same time. We can now formulate the problem.  Problem   III.3.   Given a team of   m   robots modeled as transition systems   T i ,   i   = 1 , . . . , m , and an LTL formula  φ sync   over   Π   in the form   (4) , synthesize individual runs   r i   for each robot such that   T π   minimizes the cost function   (3) , and   ̃ ω team , i.e., the word observed in the field, satisfies   φ sync .  Note that the runs produced by a solution to Prob. III.3 are guaranteed not to violate   φ sync   even if there is a mismatch between the weights   w i ( q, q ′ )   used for the solution of the problem and the actual traveling times observed in the field. Since    ̃ ω team   observed in the field is likely to be sub-optimal, we will also seek to bound the deviation from optimality in the field.  D. Solution Outline  In [9], we showed that the joint behavior of a robotic team can be captured by a region automaton. A region automaton, as defined next, is a finite dimensional transition system that captures the relative positions of the members of the robotic team. This information is then used for computing optimal trajectories.  Definition III.4   ( Region Automaton).   The region automa- ton   R   is a TS (Def. II.1)   R   := ( Q R , q 0 R , δ R ,   Π R ,   L R , w R ) , where  (i)   Q R   is the set of states of the form   ( q, r )   such that  (a)   q   is a tuple of state pairs   ( q 1 q ′  1 , . . . , q m q ′  m )   where the   i th   element   q i q ′  i   is a source-target state pair from   Q i   of   T i   meaning robot   i   is currently on its way from   q i   to   q ′  i , and  (b)   r   is a tuple of clock values   ( x 1 , . . . , x m )   where the   i th   element denotes the time elapsed since robot   i   left state   q i .  (ii)   q 0 R   is the initial state that has zero-weight transitions to all those states in   Q R   with   r   = (0 , . . . ,   0)   and   q   = ( q 0 1   q ′  1 , . . . , q 0  m q ′  m )   such that   q 0  i   is the initial state of   T i  and   ( q 0  i   , q ′  i )   ∈   δ i .  (iii)   δ R   is the transition relation such that a transition from  ( q, r )   to   ( q ′ , r ′ )   exists if and only if  (a)   ( q i , q ′  i ) ,   ( q ′  i , q ′′  i   )   ∈   δ i   for all changed state pairs where the   i th   element   q i q ′  i   in   q   changes to   q ′  i q ′′  i  in   q ′ ,  (b)   w i ( q i , q ′  i ) − x i   of all changed state pairs are equal to each other and are strictly smaller than those of unchanged state pairs, and  (c)   for all changed state pairs corresponding   x ′  i   in  r ′   becomes   x ′  i   = 0   and all other clock values in  r   are incremented by   w i ( q i , q ′  i )   −   x i   in   r ′ .  (iv)   Π R   =   ∪ m i =1 Π i   is the set of propositions;  (v)   L R   :   Q R   →   2 Π R   is a map giving the set of atomic propositions satisfied in a state. For a state with   q   = ( q 1 q ′  1 , . . . , q m q ′  m ) ,   L R (( q, r )) =   ∪ m i =1 L i ( q i ) ;  (vi)   w R   :   δ R   →   R ≥ 0   is   a   map   that   assigns   a non-negative   weight   to   each   transition   such   that  w R (( q, r ) ,   ( q ′ , r ′ )) =   w i ( q i , q ′  i ) − x i   for each state pair that has changed from   q i q ′  i   to   q ′  i q ′′  i   with a correspond- ing clock value of   x ′  i   = 0   in   r ′ .  Example III.5.   Fig. 2 illustrates the region automaton   R  that corresponds to the robots modeled with   T 1   and   T 2  given in Fig. 1. There is a transition from   (( ba, bc ) ,   (0 ,   0))  to   (( ba, cb ) ,   (1 ,   0))   with weight   1   in   R   because   ( b, c )   ∈   δ 2 ,  w 2 ( b, c ) = 1 , and   w 1 ( b, a )   6   = 1 .  Our solution to Problem III.3 can be outlined as follows: (i) We check if the LTL formula   φ sync   is trace-closed guaranteeing that it will not be violated in the field (See Sec. IV-A); (ii) We prepare the serialized region automaton of the robotic team with synchronization points by modifying the output of our earlier algorithm O BTAIN -R EGION - A UTOMATON   [9] (See Sec. IV-B); (iii) We find optimal runs on individual   T i s   using the O PTIMAL -R UN   algorithm we previously developed in [16] and use a synchronization protocol to calculate an upper bound on the cost function (3) for given deviation values to obtain the solution to Prob. III.3 (See Sec. IV-C). IV. P ROBLEM   S OLUTION  In this section, we explain each step of the solution to Prob. III.3 in detail. In the following, we use a simple example to illustrate ideas as we develop the theory for the general case. We present an experimental evaluation of our approach considering a more realistic scenario in Sec. V.
A. Trace-Closedness of the Original Formula  Prop. IV.1 shows how trace-closedness of   φ sync   guarantees correctness in the field. In the following, we say an LTL formula   φ sync   is trace-closed if the language   L B   of the corresponding B ̈ uchi automaton is trace-closed in the sense of Def. II.8.  Proposition IV.1.   If the general specification   φ sync   is a trace-closed formula with respect to the distribution given by the robots’ capabilities, then it will not be violated in the field due to uncertainties in the speeds of the robots. Proof.   From Defs. II.8 and III.1, we know that if we can find a run that satisfies a trace-closed LTL formula, then the word   ω team   produced by the run will not be a critical word. Since   ω team   is not a critical word,   6   ∃    ̃ ω team   ∈   [ ω team ]   such that    ̃ ω team   6   ∈   L B . Thus, regardless of the   ρ i   values of the robots,   φ   will not be violated in the field due to robot timing errors as any    ̃ ω team   ∈   [ ω team ]   will also be in   L B .     Thus, in order to guarantee correctness in the field, we first check that   φ sync   is trace-closed using an algorithm adapted from [17]. However, as trace-closedness is not well-defined for words over   2 Π , we construct a B ̈ uchi automaton whose language   L B   is over the set   Π .  Example   IV.2.   Fig. 1 illustrates the environment where two robots are expected to satisfy a task given by a for- mula in the form of   (4)   where   φ   =   GF r1P   ∧   GF r2P ,  Π 1   =   { r1P , π,   Sync } ,   Π 2   =   { r2P , π,   Sync } , and   Π =  { r1P ,   r2P , π,   Sync } . a  b T 1   ⇡  2   2  r1P  (a) a  b   ⇡ T 2  c  2  2  1   1  r2P   (b) Fig. 1: TS’s   T 1   and   T 2   of two robots in an environment with three vertices. The states correspond to vertices   { a, b, c } , the edges represent the motion capabilities of each robot, and the weights represent the traveling times between any two vertices. The propositions   r1P ,   r2P   and   π   are shown next to the vertices where they can be satisfied by the robots.  After checking that   φ sync   is trace-closed, we proceed by obtaining the serialized region automaton with synchroniza- tion points where the   Sync   proposition is satisfied.  B. Obtaining the Serialized Region Automaton with Synchro- nization Points  If   φ sync   is a trace-closed formula, we obtain the region automaton that captures the joint behavior of the robotic team using O BTAIN -R EGION -A UTOMATON   [9]. Next, using Alg. 1, we first introduce synchronization states by adding the special   Sync   proposition to the states where all robots occupy some vertex in their TS’s simultaneously,   i.e. , states with   r   = (0 , . . . ,   0) . Note that, these are the states that will ab, ab  (0 ,   0)  ba, ba  (0 ,   0)  ba, bc  (0 ,   0)  ba, cb  (1 ,   0)  ⇡  ab, bc  (0 ,   0)  ab, cb  (1 ,   0)  ab, ba  (0 ,   0)  ba, ab  (0 ,   0)  R  2   1 2   2  1  1  2 2 2 1  1  1  q   0  R  0  r1P  r2P   ⇡  r1P  r2P  ⇡  r2P  ⇡  r2P  ⇡  r1P  Fig. 2: Region automaton obtained using O BTAIN -R EGION -A UTOMATON  [9] that captures the joint behavior of the robotic team given in Fig. 1.   Sync  states where all robots occupy vertices,   i.e. , states with all zero clock values, are highlighted in blue.  be used to calculate a bound on optimality when the robots are deployed in the field. We then expand the states where multiple propositions are satisfied simultaneously to obtain  R ser   where at most one proposition is satisfied at each state. This ensures that languages of both the B ̈ uchi automaton that corresponds to   φ sync   and   R ser   are over   Π .  Example IV.2 Revisited.   Fig. 2 illustrates the region au- tomaton   R   that captures the joint behavior of the team given in Fig. 1. The serialized region automaton with synchroniza- tion points   R ser   that corresponds to   R   is given in Fig. 3. ab, ab  (0 ,   0)  ba, ba  (0 ,   0)   ba, bc  (0 ,   0) ⇡  ab, bc  (0 ,   0)  ab, cb  (1 ,   0)  ab, ba  (0 ,   0)  ba, ab  (0 ,   0)  R   ser  2   1  2   2  1  1  2 2 2  1  1 1  q   0  R  0  r1P   r2P  ⇡  r1P   r2P  ⇡ r2P   ⇡ r2P  ⇡   r1P  ba, ba  (0 ,   0)  ba, ba  (0 ,   0)  ba, bc  (0 ,   0)  ba, bc  (0 ,   0)  ab, ba  (0 ,   0)  ba, ab  (0 ,   0)  ba, ab  (0 ,   0)  Sync  ab, ba  (0 ,   0)  Sync  ba, ba  (0 ,   0)  Sync  ba, bc  (0 ,   0)  Sync  Sync  ab, bc  (0 ,   0)   ab, bc  (0 ,   0)  Sync  ba, cb  (1 ,   0)  Fig. 3: Serialized region automaton with synchronization states obtained after applying Alg. 1 to   R   in Fig. 2. New states introduced after serialization are highlighted in blue. Red arrows stand for zero-weight transitions.  Remark IV.3.   Since   φ sync   is trace-closed, the serialization can be done in any order. Since all possible orderings belong to the same trace-equivalent class, they do not affect the satisfaction of the formula. C. Finding the Robust Optimal Run and the Optimality Bound  After obtaining the serialized region automaton   R ser   , we find an optimal run   r ?  R   on   R ser   that minimizes the cost function (3) using our earlier O PTIMAL -R UN   algorithm [16]. The optimal run   r ?  R   is always in a prefix-suffix form (Def. II.4). Furthermore, as   r ?  R   satisfies   φ sync , it has at least one synchronization point in its suffix cycle, which we assume to start with a synchronization point.  Definition IV.4   ( Projection of a run on   R   to   T i s).   Given  T   and the corresponding run   r R   on   R ser   where  r R   = (( q 0 1   q 1 1   , . . . , q 0  m q 1  m ) ,   ( x 0 1 , . . . , x 0  m )) (( q 1 1   q 2 1   , . . . , q 1  m q 2  m ) ,   ( x 1 1 , . . . , x 1  m ))   . . . ,
Algorithm 1:   S ERIALIZE -R EGION -A UTOMATON  Input : A region automaton   R   obtained using O BTAIN -R EGION -A UTOMATON   .  Output :   R ser   , the serialized region automaton with synchronization states, such that at most one proposition is satisfied at each state.  1   foreach   State   { q, r }   in   R   do  2   if   r   = (0 , . . . ,   0)   then  3   Add   Sync   to propositions satisfied in   { q, r } .  4   k   ←−   Number of propositions satisfied in   { q, r } .  5   if   k >   1   then  6   propsT uple   ←   The tuple   ( p 1 , . . . ,   p k )   of propositions satisfied in   { q, r } .  7   Copy   { q, r }   k   times to obtain   { q, r } ′  1 , . . . ,   { q, r } ′  k .  8   foreach   i   = 1 , . . . , k   do  9   L ( { q, r } ′  i )   ←   propsT uple [ i ] .  10   if   i < k   then  11   Add   { q, r } ′  i   → { q, r } ′  i +1   to   δ R   with zero weight.  12   Re-direct all incoming transitions of   { q, r }   to  { q, r } ′  1 .  13   Originate all outgoing transitions of   { q, r }   from  { q, r } ′  k .  14   Remove   { q, r }   from   Q R .  we define its projection on   T i   as run   r i   =   q 0  i   q 1  i   . . .   for all  i   = 1 , . . . , m , where   q k i   only appears in   r i   if   x k i   = 0   and  T ( k )   6   =   T ( k   + 1) .  In [9] we show that the individual runs   r i   obtained by the projection in Def. IV.4 are equivalent to the region automaton run   r R   in the sense that they produce the same word   ω team . Using Def. IV.4, we project the optimal run   r ?  R   to individual  T i s to obtain the set of optimal individual runs   { r ?  1   , . . . , r ? m } . As the robots execute their infinite runs in the field, they synchronize with each other at the synchronization point following the protocol given in Alg. 2 ensuring that they start each new suffix cycle in a synchronized way. Using this protocol, we can define a bound on optimality,   i.e. , the value of the cost function (3) observed in the field, as given in the following proposition.  Proposition IV.5.   Suppose that each robot’s deviation value is bounded by   ρ >   0   (i.e.,   ρ i   ≤   ρ   for all robots   i ), and let  J ( T π   )   be the cost of the planned robot paths. Then, if the robots follow the protocol given in Alg. 2 the field value of the cost satisfies  J ( T π   )   ≤   J ( T π   ) +   ρ ( J ( T π   ) + 2 d s ) ,  where   d s   is the planned duration of the suffix cycle. Proof.   In   the   following,   we   take   the   suffix   to   begin   at a synchronization point. The suffix consists of an infinite number of repetitions of the suffix cycle, which we denote  Algorithm 2:   S YNC -R UN  Input : A run   r k   of robot   k   in the prefix-suffix form with at least one synchronization point in its suffix cycle.  1   begin  2   syncP oint   ←   First synchronization point in the suffix.  3   teamF lags   ←   (0 , . . . ,   0) .  4   while   True   do  5   if   syncM essage   received from robot   i   then  6   teamF lags [ i ]   ←   1 .  7   if   currentState   =   syncP oint   then  8   Stop  9   Broadcast   syncM essage .  10   teamF lags [ k ]   ←   1 .  11   if   teamF lags   = (1 , . . . ,   1)   then  12   teamF lags   ←   (0 , . . . ,   0) .  13   Continue executing   r k .  S c . Let   d s   be the planned duration of   S c , let   n s   be the number of optimizing propositions satisfied in   S c . Let us redefine  t   = 0   to be the time when the suffix starts, and let    ̄ T π  be a sequence of length   n s   recording the   n s   times that the optimizing proposition is satisfied on the first repetition of  S c . Note that, as we consider infinite runs and as the process restarts itself at the beginning of each   S c   by means of the synchronization protocol given in Alg. 2, we only need to consider the first repetition of   S c . We first define  T   i   =  ̄ T π   ( i )(1   −   ρ )  T   i   =  ̄ T π   ( i )(1 +   ρ )  t w   =   d s (1 +   ρ )  where,   T   i   and   T   i   are the earliest and latest times that the  i th optimizing proposition can be satisfied, respectively. The value   t w   is the latest time that the second repetition of   S c   can begin. Then, for   0   < i   ≤   n s , the worst-case time between satisfying the   i th optimizing proposition and the   ( i   + 1) th optimizing proposition is  τ   i,i +1   =  {  T   i +1   −   T   i   if   0   < i < n s ,  t w   +   T   1   −   T   n s   if   i   =   n s .   (5) Next, in the planned paths, multiple robots may simultane- ously satisfy the   i th optimizing proposition. In the field, these satisfactions will not occur simultaneously. The maximum amount of time between the first and last of these satisfying instances for the   i th proposition, for   0   < i   ≤   n s , is  τ   i   =   T   i   −   T   i .   (6) Finally, using (5) and (6) we obtain the upper bound on the value of the cost function (3) that will be observed during deployment as  J ( T π   ) = max { max  i   { τ   i,i +1 } ,   max  i   { τ   i }} .   (7)
Substituting the definitions for   T   i ,   T   i , and   t w   into (5) we obtain   τ   i,i +1   =  {  ̄ T π   ( i   + 1)(1 +   ρ )   −    ̄ T π   ( i )(1   −   ρ )   if   0   < i < n s ,  (1 +   ρ ) ( d s   +  ̄ T π   (1) )   −    ̄ T π   ( n s )(1   −   ρ )   if   i   =   n s  But, we have that   J ( T π   )   ≥    ̄ T π   ( i   + 1)   −    ̄ T π   ( i ) , and   J ( T π   )   ≥  d s   +  ̄ T π   (1)   −    ̄ T π   ( n s ) . In addition,    ̄ T π   (1)   ≤   J ( T π   )   and   ̄ T π   ( i )   ≤   d s   for all   i   ∈ { 2 , . . . , n s } . Using these expressions we obtain  τ   i,i +1   ≤   J ( T π   ) +   ρ ( J ( T π   ) + 2 d s ) .  Similarly, we get  τ   i   ≤   2 ρd s ,  and thus   J ( T π   )   ≤   J ( T π   ) +   ρ ( J ( T π   ) + 2 d s ) .     Remark IV.6.   In Prop. IV.5, we have provided a conser- vative bound for ease of presentation. However, we can calculate an exact bound on the field value of the cost   J ( T π   )  using a treatment similar to the proof of Prop IV.5.  Example IV.2 Revisited.   For the example we have shown throughout this section, applying Alg.   O PTIMAL -R UN   [16] to   R ser   given in Fig. 2 and the formula   φ sync   :=   GF r1P   ∧  GF r2P   ∧   GF π   ∧   GF Sync   results in the optimal run with the prefix  T   0   2   2   2   2   3  r ?  R  ab,ab   ba,bc   ba,bc   ba,bc   ba,bc   ba,cb (0,0)   (0,0)   (0,0)   (0,0)   (0,0)   (1,0)  L R ( · )   Sync   r1P   Sync   r2P   π and the suffix cycle  T   4   4   4   6   6   6  r ?  R  ab,ba   ab,ba   ab,ba   ba,ab   ba,ab   ba,ab (0,0)   (0,0)   (0,0)   (0,0)   (0,0)   (0,0)  L R ( · )   r2P   Sync   π   r1P   Sync   π which will be repeated an infinite number of times. In the ta- ble above, the rows correspond to the times when transitions occur, the run   r ?  R , and the satisfying atomic propositions, respectively. For this example,   T π   = 2 ,   4 ,   6 ,   8 ,   10 , . . .   and the cost as defined in   (3)   is   J ( T π   ) = 2 . Furthermore, when the robotic team is deployed in the field, this cost is bounded from above by 2.5 for   ρ 1   =   ρ 2   = 0 . 05   as given by Prop. IV.5. Applying Def. IV.4 to   r ?  R   we have the following individual runs:  T   0   2   3   4   6   8   10   . . .  r ?  1   a   b   a   b   a   b   . . .  r ?  2   a   b   c   b   a   b   a   . . . Note that, at time   t   = 3 , the second robot has arrived at   c  while the first robot is still traveling from   b   to   a , therefore the clock of the first robot is not zero at this time, i.e.,   x 1   6   = 0 , and   b   does not appear in   r ?  1   at time   t   = 3 .  We finally summarize our approach in Alg. 3, show that this algorithm indeed gives a solution to Prob. III.3 and analyze the overall complexity of our approach.  Proposition IV.7.   Alg. 3 solves Prob. III.3. Proof.   Note that Alg. 3 combines all steps outlined in this section. The planned word   ω team   generated by the entire  Algorithm 3:   R OBUST -M ULTI -R OBOT -O PTIMAL -R UN  Input :   m   T i ’s and a global LTL specification   φ sync   of form (4).  Output : A set of robust optimal runs   { r ?  1   , . . . , r ? m }   that satisfies   φ sync , minimizes (3), and the bound on the performance of the team in the field.  1   begin  2   φ sync   :=   φ   ∧   GF π   ∧   GF Sync .  3   if   φ sync   is trace - closed   then  4   Obtain the region automaton   R   using O BTAIN -R EGION -A UTOMATON   [9].  5   Obtain   R ser   using S ERIALIZE -R EGION -A UTOMATON   .  6   Find the optimal run   r ?  R   applying O PTIMAL -R UN  [16] to   R ser   and   φ sync .  7   Obtain individual runs from   r ?  R   using Def. IV.4.  8   Find the bound on optimality as given in Prop. IV.5.  9   else  10   Abort. team satisfies   φ sync   and minimizes (3), as shown in [9]. Furthermore, since   φ sync   is trace-closed, the optimal satisfy- ing run is guaranteed not to violate   φ sync   in the field due to timing errors as given in Prop. IV.1. Therefore,   { r ?  1   , . . . , r ? m }  as obtained from Alg. 3 is the solution to Prob. III.3.     Proposition IV.8.   For the case where a group of   m   identical robots are expected to satisfy an LTL specification   φ   in a common environment with   ∆   edges and a largest edge weight of   W   , the worst-case complexity of Alg. 3 is   O ((∆   ·   W   ) 3 m   ·  2 O ( | φ | ) ) . Proof.   From [9], the number of states of the region automa- ton   R   is bounded by  (   m ∏  i =1  | δ i |  ) (   m ∏  i =1  W i   −  m ∏  i =1  ( W i   −   1)  )  + 1  where   m   is number of robots and   W i   is largest edge weight in TS   T i   of robot   i . Then, for the above mentioned case, the worst-case size of the region automaton is   O ((∆   ·   W   ) m )  . In [8], the authors give the worst-case complexity of the O PTIMAL -R UN   algorithm as   O ( | T   | 3   ·   2 O ( | φ | ) )   where   | T   |   is the number of states of the input transition system and   | φ |   is the length of the LTL specification. Therefore, the worst-case complexity of Alg. 3 becomes   O ((∆   ·   W   ) 3 m   ·   2 O ( | φ | ) ) .     V. I MPLEMENTATION AND   C ASE   S TUDIES  We implemented Alg. 3 in objective-C as the software package LTL R OBUST   O PTIMAL   M ULTI - ROBOT   P LANNER  (LROMP)   and   used   it   in   conjunction   with   our   earlier O PTIMAL -R UN   [16] algorithm to obtain robust and optimal trajectories   for   robots   performing   persistent   data   gather- ing   missions   in   a   road   network   environment.   The   soft- ware package, available at   http://hyness.bu.edu/
(a) 1   CCW  2   CCW  8   3   CCW  4   CW  5   CW  6   CW  9 7  1   CW  2   CW  3   CW  4   CCW  5   CCW  6   CCW  3  2  3  2  2  3  1  1  1  1  1  1  3  2  3  2  2  3  6  6  6  6  4  4  4  4  4  4  4  4  (b) Fig. 4: (a) Road network used in the experiments (b) The model of the road network with weights shown in blue. 1 time unit in this model corresponds to 3 seconds. The red and blue regions are data gathering locations of robots 1 and 2, respectively and the green region is the common upload location. CW and CCW stand for clockwise and counter-clockwise, respectively.  Software.html , utilizes the dot tool [18] to visualize transition systems and the O PTIMAL -R UN   algorithm uses the LTL2BA software [19] to convert LTL specifications to B ̈ uchi automata. Following the steps detailed in Sec.IV, the software first creates the serialized region automaton with synchronization states   R ser   using   T i s defined by the user and exports an M-file which defines   R ser   in Matlab. Next,  φ sync   is checked for trace-closedness, after which O PTIMAL - R UN   algorithm is executed in Matlab to find the optimal run   r ?  R   on   R ser   . Finally, an upper bound on the field value of the cost function (3) is computed and   r ?  R   is projected to individual   T i ,   i   = 1 , . . . , m , to obtain the solution to Prob. III.3. Fig. 4 illustrates our experimental platform, which is a road network consisting of roads, intersections, and task locations. The figure also shows the transition system that models the motion of the robots on this road network where 1 time unit corresponds to 3 seconds. In the following, the transition systems   T i   are identical except for their initial states and the sets of propositions that can be satisfied at states. In our experiments, we consider a persistent monitoring task where two robots with deviation values of   ρ 1   = 0 . 09 ,  ρ 2   = 0 . 04   repeatedly gather and upload data and the maxi- mum time in between any two data uploads must be mini- mized. We require robots 1 and 2 to gather data at 7 and 8 in Fig. 4, respectively and upload the data at 9. We define   Π =  { R1Gather ,   R1Upload ,   R2Gather ,   R2Upload ,   Upload ,  Sync }   and assign the atomic propositions as  L 1 (7) =   { R1Gather } ,   L 1 (9) =   { R1Upload ,   Upload } L 2 (8) =   { R2Gather } ,   L 2 (9) =   { R2Upload ,   Upload } .  where   Upload   is set as the optimizing proposition ( π   as in formula (4)) due to the task specification. Next, we forbid  Fig. 5: Team trajectories used in the experiments. The red and blue regions are data gathering locations of robots 1 and 2, respectively and the green region is the common upload location. The circles on the left show the sync point,   i.e. , the beginning of the suffix cycle, on the trajectories of the robots.  data uploads unless robots have something to upload using the LTL formula  φ   =   G ( R1Upload   ⇒   X ( ¬ R1Upload   U   R1Gather ))  ∧   G ( R2Upload   ⇒   X ( ¬ R2Upload   U   R2Gather )) .  Our overall LTL formula in the form of (4) is  φ sync   =   φ   ∧   G F   Upload   ∧   G F   Sync .   (8) Running our algorithms on an iMac i5 quad-core com- puter, we obtain the robust optimal trajectory as illustrated in Fig. 5. The algorithm ran for 35 minutes, and the region automaton   R ser   had 5224 states. The value of the cost function was 19 time units (57 seconds) with an upper- bound of 27.55 time units (82.65 seconds), meaning that the maximum time in between data uploads would be less than 82.65 seconds in the field. This result was experimentally verified in our robotic test-bed and the maximum time in between data uploads was measured to be 64 seconds (21.3 time units) during a run of 13 minutes. In order to confirm and demonstrate the effectiveness of our approach, we exe- cuted the same trajectory without any synchronization. After approximately 6.5 minutes, the maximum time in between data uploads was measured to be 92 seconds (30.7 time units), much worse than what is provided by our approach. Our video submission accompanying the paper displays the robot trajectories for both cases. It is interesting to note that, in the optimal solution the second robot spends extra time spinning between states   4 CW  and   4 CCW   (Figs. 4b, 5). This behavior is actually time- wise optimal as it decreases the maximum time between successive satisfying instances of the optimizing proposition. VI. C ONCLUSIONS  In this paper we presented and experimentally evaluated a method for planning robust optimal trajectories for a team of robots that satisfy a common temporal logic mission specification. Our method is robust to uncertainties in the traveling times of each robot, and thus has practical value in applications where multiple robots must perform a series of tasks collectively in a common environment. We considered trace-closed temporal logic formulas with optimizing and
synchronizing propositions that must be repeatedly satisfied. In the absence of timing errors, the motion plan delivered by our method is optimal in the sense that it minimizes the maximum time between satisfying instances of the optimiz- ing proposition. If the traveling times observed in the field deviate from those given by the transition systems of the robots, our method guarantees that the mission specification is   never   violated   and   provides   an   upper   bound   on   the ratio between the performance in the field and the optimal performance. A CKNOWLEDGMENTS  We thank Jennifer Marx at Boston University for her work on the experimental platform. R EFERENCES [1]   S.   G.   Loizou   and   K.   J.   Kyriakopoulos,   “Automatic   synthesis   of multiagent motion tasks based on LTL specifications,” in   IEEE Conf. on Decision and Control , Paradise Island, Bahamas, 2004, pp. 153– 158. [2]   H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Temporal logic- based reactive mission and motion planning,”   IEEE Transactions on Robotics , vol. 25, no. 6, pp. 1370–1381, 2009. [3]   T. Wongpiromsarn, U. Topcu, and R. M. Murray, “Receding horizon control for temporal logic specifications,” in   Hybrid systems: Compu- tation and Control , Stockholm, Sweden, 2010, pp. 101–110. [4]   A. Bhatia, L. E. Kavraki, and M. Y. Vardi, “Motion planning with hybrid dynamics and temporal goals,” in   IEEE Conf. on Decision and Control , 2010, pp. 1108–1115. [5]   L. Bobadilla, O. Sanchez, J. Czarnowski, K. Gossman, and S. LaValle, “Controlling wild bodies using linear temporal logic,” in   Proceedings of Robotics: Science and Systems , Los Angeles, CA, USA, June 2011. [6]   M.   Y.   Vardi   and   P.   Wolper,   “An   automata-theoretic   approach   to automatic program verification,” in   Logic in Computer Science , 1986, pp. 322–331. [7]   G. Holzmann, “The model checker SPIN,”   IEEE Transactions on Software Engineering , vol. 25, no. 5, pp. 279–295, 1997. [8]   S. L. Smith, J. T ̊ umov ́ a, C. Belta, and D. Rus, “Optimal path planning for surveillance with temporal logic constraints,”   International Journal of Robotics Research , vol. 30, pp. 1695–1708, Dec. 2011. [9]   A. Ulusoy, S. L. Smith, X. C. Ding, C. Belta, and D. Rus, “Optimal path planning for surveillance with temporal logic constraints,” pp. 3087–3092, Sep. 2011. [10]   M. Kloetzer and C. Belta, “Automatic deployment of distributed teams of robots from temporal logic specifications,”   IEEE Transactions on Robotics , vol. 26, no. 1, pp. 48–61, 2010. [11]   R. Milner,   Communication and concurrency .   Prentice-Hall, 1989. [12]   A. Puri, “An undecidable problem for timed automata,”   Discrete Event Dynamic Systems , vol. 9, no. 2, pp. 135–146, 2000. [13]   ——,   “Dynamical   properties   of   timed   automata,”   Discrete   Event Dynamic Systems , vol. 10, no. 1-2, pp. 87–113, 2000. [14]   L. C. G. J. M. Habets and J. H. van Schuppen, “A control problem for affine dynamical systems on a full-dimensional polytope,”   Automatica , vol. 40, pp. 21–35, 2004. [15]   Y. Chen, X. C. Ding, and C. Belta, “A formal approach to the deploy- ment of distributed robotic teams,”   IEEE Transactions on Robotics , 2011, to appear. [16]   S. L. Smith, J. T ̊ umov ́ a, C. Belta, and D. Rus, “Optimal path planning under temporal logic constraints,” in   IEEE/RSJ Int. Conf. on Intelligent Robots & Systems , Taipei, Taiwan, Oct. 2010, pp. 3288–3293. [17]   D. Peled, T. Wilke, and P. Wolper, “An algorithmic approach for check- ing closure properties of temporal logic specifications and omega- regular languages,”   Theor. Comput. Sci. , vol. 195, no. 2, pp. 183–203, 1998. [18]   “Graphviz - graph visualization software,” http://www.graphviz.org/. [19]   “LTL2BA,” http://www.lsv.ens-cachan.fr/ ∼ gastin/ltl2ba/index.php.