Executing a Golog program on an actual robot typically requires additional platform constraints to be satis ed. Such constraints are often temporal, refer to metric time, and require modi cations to the abstract Golog program. Based on ES and ESG, modal variants of the Situation Calculus, we propose the logic t -ESG, a logic which allows the speci cation of metric temporal constraints for Golog programs. We provide a comparison to ESG and show that Metric Temporal Logic (MTL) can be embedded into t -ESG. We show how to formulate constraints using a model of the robot platform, and we sketch a procedure that solves those constraints using Simple Temporal Networks (STNs).
While Golog [14], an agent programming language based on the Situation Calculus [15, 20], allows a clear and abstract speci cation of an agent's behavior, executing a Golog program on a real robot often creates additional issues. Typically, the robot's platform requires additional constraints that are ignored when designing a Golog program. As an example, a robot needs to calibrate its arm before it can use it, and it needs to enable its perception module before it interacts with its environment. Developers typically face two options: First, they can directly model all the platform details in the basic action theory (BAT) and add respective actions to their programs, e.g., they can enable the perception before a pick action and disable it afterwards again. However, this makes the behavior speci cation much more complex and errorprone. If the program involves some form of planning or search, the platform details may cause performance degradation, as the search space's size is increased by the additional actions. Additionally, most of these platform details are not speci c to one particular program, but to the platform. Any change to the platform needs to be re ected in the behavior speci cation. As an alternative, the developers may decide to use Golog for an abstract behavior speci cation and deal with the platform details on the lower levels. However, this is often not possible, as platform constraints require changes to the high-level program, and thus the program cannot be clearly separated from the platform it is running on.
In this paper, we propose a di erent approach: As before, the agent's behavior is speci ed with an abstract program. However, based on platform models as shown in Figure 1, we construct a maintenance BAT that allows to specify a set of additional constraints on the platform. The abstract plan from the original Golog program is then transformed into an executable action sequence that satis es the platform constraints.
The main ideas of this approach were sketched in [10]. In the following, we focus on the logical foundations that allow the speci cation of metric temporal constraints. Our starting point is the logic ESG [6], a temporal variant of ES [13], which in turn is a modal variant of the Situation Calculus. We extend ESG by metric time, quantitative temporal operators similar to Metric Temporal Logic (MTL) [12], and additional temporal operators previous and since, which refer to past states in the same way as next and until refer to future states. We show the relationship between ESG and t -ESG and we provide an embedding of MTL into t -ESG. Next, we show how to describe a BAT and an
start calibrate()
5s abstract Golog program in t -ESG and how to formulate metric temporal platform constraints with t -ESG. Finally, we sketch how to resolve those constraints with a Simple Temporal Network (STN) to transform the abstract program into an executable action sequence. 2
The Situation Calculus [15, 20] is a rst-order logic for representing and reasoning about actions. Action preconditions and e ects are axiomatized with basic action theories and situations are histories of actions, e.g., the situation term do(pick (o1); S0) refers to the situation after doing action pick (o1) in the initial situation. The programming language Golog [14] is based on the Situation Calculus and o ers imperative programming constructs such as sequences of actions and iteration as well as non-deterministic branching and non-deterministic choice. The semantics of Golog and its on-line variant IndiGolog can be speci ed in terms of transitions [7].
The logic ES [13] is a modal variant of the Situation Calculus which gets rid of explicit action terms and uses modal operators instead. As an example, [pick (o1)]Holding (o1) is satis ed i Holding (o1) is true after doing pick (o1). The logic ESG [6, 5] is a temporal extension of ES for the veri cation of Golog programs. It speci es program transition semantics similar to the transition semantics of IndiGolog and extends ES with the temporal operators X (next ) and U (until ).
The Situation Calculus has also been extended by a notion of time. Reiter requires each action A to have an explicit time argument, i.e., each action is of the form A(~x; t) [19]. Durative actions are modeled with start and stop actions, and the time of the last occurrence of an action can be referred by time(A(~x; t)). Reiter also extends the Situation Calculus with concurrency, e.g., do(fend pick (o1); start goto(kitchen)g; s) refers to the situation after ending the action pick (o1) and at the same time start moving to the kitchen. A similar approach is described by [18], which also allows temporal reasoning about situations. In particular, they di erentiate between possible and actual evolvements of the current situation by adding axioms for a distinct predicate actual , where actual (s) is true i s is an actual evolvement of the world. This di erentiation is important, because otherwise, we could not express much about the future; as long as there is a possible action that causes a formula to be false, we cannot state that is true in the next situation, even if the agent has no intention (e.g., it is not the next action in the Golog program) to execute the action. As we will see, this problem does not occur in ESG or t -ESG.
MTL [12] is an extension of Linear Time Logic (LTL) with metric time, which allows expressions such as F c , meaning eventually within time c. In MTL, formulas are interpreted over timed words or timed state sequences, where each state speci es which propositions are true, and each state has an associated time value. Depending on the choice of the state and time theory, the satis ability problem for MTL becomes undecidable [2]. However, for nite words, it has been shown to be decidable [16]. MTL has been restricted to Metric Interval Temporal Logic (MITL) [3], which prohibits singular intervals and is interpreted over time intervals instead of time points, which makes the satis ability problem for MITL decidable. MTLP [4] is an extension of MTL with temporal operators referring to the past, e.g., V (preVious ) and S (Since).
Simple Temporal Networks (STNs) [8] provide an e cient procedure to solve a constraint problem given by a set of time-points ftig and a set of binary temporal constraints of the form tj ti . Disjunctive Linear Relations (DLRs) [11] allow more expressive temporal constraints; the restricted Horn DLRs can be solved in polynomial time and still subsume STNs.
Similar to the proposed approach, Schi er, Wortmann, and Lakemeyer extend Golog for selfmaintenance [21] by allowing temporal constraints using Allen's Interval Algebra [1]. Those constraints are resolved on-line by interleaving the original program with maintenance actions. Closely related is also the work by [9], who propose a hybrid approach of temporal constraint reasoning and reasoning about actions based on the Situation Calculus. Similar to [21], they allow constraints based on Allen's Interval Algebra, which are translated into a temporal constraint network. 3
Timed ESG In this section, we present the syntax and semantics of t -ESG. As t -ESG is based on ESG, its syntax and semantics are also based on ESG and ES. We refer to [13, 6, 5] for more details on the original syntax and semantics. De nition 1 (Language of t -ESG). The language consists of formulas over symbols from the following vocabulary: 1. object variables x1; x2; x3; : : : ; y1; : : : 2. action variables a; a1; a2; a3; : : : 3. number variables t1; t2; t3; : : : 4. object standard names NO = fo1; o2; o3; : : :g 5. action standard names NA = fp1; p2; p3; : : :g 6. number standard names NN here, we assume NN = Q = f0; 1; 2; 12 ; : : :g; 7. uent predicates of arity k: F k : ff1k; f2k; : : :g, e.g., Holding ; we assume this list contains the distinguished predicates Poss and < 8. rigid functions of arity k: Gk = fg1k; g2k; : : :g, e.g., goto; including distinguished functions +; 2 G2 9. uent object functions of arity k: fh1k; h2k; : : :g, e.g., parent H k = 10.
uent number functions of arity k: Ik = ik; i2k; : : :g, e.g., battery ; including distinguished ffu1nctions time 2 I1 and now 2 I0 11. open, closed, and half-closed intervals, e.g., [1; 2], with constants of sort number as interval endpoints 12. connectives and other symbols: =, ^, _, :, 8,
XI ;VI , UI , SI (with interval I), , [ ], J K We also write F for the set Sk2N0 F k, similarly for G; H; I. We also denote the set of standard names as N = NO [ NA [ NN . Furthermore, we call a term primitive if it is of the form f (n1; : : : ; nk), with f; ni being standard names. We denote the set of primitive terms as PO (objects), PA (actions), and PN (numbers), and P = PO [ PA [ PN .
We read XI as next (within interval I), VI as previously (within interval I), UI as until (within interval I), and SI as since (within interval I). De nition 2 (Terms of t -ESG). The set of terms of t -ESG is the least set such that every variable is a term of the corresponding sort, every standard name is a term of the corresponding sort, if t1; : : : ; tk are terms and f is a k-ary function symbol, then f (t1; : : : ; tk) is a term of the same sort as f .
De nition 3 (Programs).
::= t j where t is an action term and is a static situation formula. A program consists of primitive actions t, tests ?, sequences 1; 2, nondeterministic branching 1j 2, nondeterministic choice of argument x: , interleaved concurrency 1k 2, and nondeterministic iteration . De nition 4 (Situation Formulas). The situation formulas are the least set such that 1. if t1; : : : ; tk are terms and P is a k-ary predicate symbol, then P (t1; : : : ; tk) is a situation formula, 2. if t1 and t2 are terms, then (t1 = t2) is a situation formula, 3. if and are situation formulas, x is a variable, P is a predicate symbol, is a program, and is a trace formula, then ^ , : , 8x: , , [ ] , and J K are situation formulas.
We call a situation formula of the form P (n1; : : : ; nk) with ni 2 N a primitive formula and denote the set of primitive formulas as PF .
De nition 5 (Trace Formulas). The trace formulas are the least set such that 1. if is a situation formula, then it is also a trace formula, 2. if and are trace formulas, x is a variable, and I is an interval, then ^ , : , 8x: , XI , VI ,
SI , and UI are also trace formulas.
We also write < c, c, = c, > c, and c for the respective intervals [0; c), [0; c], [c; c], (c; 1), and [c; 1). We use the short-hand notation FI def = (future) and GI :FI : (globally ), as well as PI d=ef (> UI ) (past ) and HI d=ef :PI : (historically ). For intervals, c + [s; e] denotes the interval [s+c; e+c], similarly for c+(s; e), c+[s; e), and c+(s; e]. We also omit the interval I if I = [0; 1), e.g., U is short for d=ef (> UI )
De nition 6 (Static Formulas). A situation formula is static if it contains no [ ], , or J K operators. De nition 7 (Bounded Formulas). A situation formula is bounded if it contains no or J K operators, and [t] operators only in case the argument is an atomic action t.
De nition 8 (Fluent Formulas). A situation formula is uent if it is static and contains no predicate Poss. The language of t -ESG extends the language of ESG by the constrained temporal operators XI and UI . Also, ESG has no operators referring to the past; i.e., no V or S (or their constrained variants VI and SI ). Finally, as we understand X ( U ) as short-hand notation for X[0;1) ( U[0;1) ), the language of ESG is a subset of t -ESG. De nition 9 (Timed Traces). A timed trace is a possibly in nite timed sequence of action standard names with monotonically non-decreasing time. Formally, a trace is a mapping : N ! PA NN , and for any i; j 2 N with (i) = ( i; ti), (j) = ( j; tj) : If i < j, then ti tj. Also, we require the sequence (ti)i2N to be non-Zeno, i.e., it is either nite or unbounded.
For a nite timed trace z = h(a1; t1) (a2; t2) : : :
def
(ak; tk)i, we de ne time(z) = tk, i.e., time(z) is the
time value of the last action in z. We denote the set of
nite timed traces as Z, the set of in nite timed traces
as , and the set of all traces as T = Z [ .
De nition 10 (World). Intuitively, a world w
determines the truth of uent predicates as well as the
value of uent functions, not just initially, but after
any (timed) sequence of actions. Formally, a world
is a mapping w that maps (
Similar to ES and ESG, the truth of a uent after any sequence of actions is determined by a world w. Di erent to ES and ESG, we require all traces referred by a world to contain time values for each action. This also means that in the same world, a uent predicate F (~n) may have a di erent value after the same sequence of actions if the actions were executed at di erent times, i.e., w[F (~n; h(a1; 1)i] may have a di erent value than w[F (~n; h(a1; 2)i].
De nition 11 (Denotation of terms). Given a ground term t, a world w, and a timed trace z 2 Z, we de ne jtjzw by: 1. if t 2 N , then jtjzw = t, 2. if t = now , then jtjzw = time(z), 3. if t = time(a(t1; : : : ; tk)), then jtjzw = max fta j (a(n1; : : : ; nk); ta) 2 zg [ f0g, where ni = jtijzw, 4. if t = f (t1; : : : ; tk) then jtjzw = w[f (n1; : : : ; nk); z], where ni = jtijzw
Note the special denotation for the function symbols now 2 I0 and time 2 I1. The term now always refers to the current time, while time(A(~x)) refers to the time of the last occurrence of A(~x), or 0 if the action has never occurred.
De nition 12 (Program Transition Semantics). The transition relation !w among con gurations, given a world w, is the least set satisfying 1. hz; ai !w hz (p; t) ; nil i, if p = jajzw, t and w; z (nil ; t) j= Poss(p)
w w 2. hz; 1; 2i ! hz p; ; 2i, if hz; 1i ! hz p; i, 3. hz; 1; 2i !w hz p; 0i if hz; 1i 2 F w and hz; 2i !w hz p; 0i 4. hz; 1j 2wi !w hz p; 0i if hz; 1i !w hz p; 0i or hz; 2i ! hz p; 0i 5. hz; x: i !w hz p; 0i, if hz; nxi !w hz p; 0i for some n 2 Nx
w w 6. hz; i ! hz p; ; i if hz; i ! hz p; i
w w 7. hz; 1k 2i ! hz p; 0k 2i if z; 1 ! hz p; 0i w w 8. hz; 1k 2i ! hz p; 1k 0i if z; 2 ! hz p; 0i time(z), The set of nal con gurations F w is the smallest set such that 1. hz; ?i 2 F w if w; z j= , 2. hz; 1; 2i 2 F w if hz; 1i 2 F w and hz; 2i 2 F w 3. hz; 1j 2i 2 F w if hz; 1i 2 F w, or hz; 2i 2 F w 4. hz; x: i 2 F w if hz; nxi 2 F w for some n 2 Nx 5. hz; i 2 F w 6. hz; 1k 2i 2 F w if hz; 1i 2 F w and hz; 2i 2 F w The program transition semantics is very similar to the semantics of ESG. The only di erence is in Rule 1, which has an additional constraint on the time, and which requires the action to be executable.
De nition 13 (Program Traces). Given a world w and a nite sequence of action standard names z, the set k kzw of (timed) traces of a program is k kzw = f 2
where for all i
fz0 2 Z j hz; i !w hz z0; 0i and hz z0; 0i 2 F wg[
j hz; i !w hz (
i w; z 6j= 5. w; z j= 8x: i w; z j= nx for all n 2 Nx 6. w; z j= i w; z z0 j= for all z0 2 Z 7. w; z j= [ ] i for all nite z0 2 k kzw, w; z z0 j= 8. w; z j= J K i for all 2 k kzw, w; z; j= Intuitively, [ ] means that after every execution of , the situation formula is true. J K means that during every execution of , the trace formula is true.
The truth of trace formulas is de ned as follows for w 2 W, z 2 Z, and 2 T : i w; z j= and is a situation 1. w; z; j=
formula, 2. w; z; j= ^ i w; z; j= and w; z; j= , 3. w; z; j= :
i w; z; 6j= , 4. w; z; j= 8x: i w; z; j= xn for all n 2 Nx, 5. w; z; j= XI i there is p 2 PA with = p w; z p; 0 j= , and time(p) 2 time(z) + I, 0, 6. w; z; w; z0; p j= VI i z = z0 p for some p 2 PA,
j= , and time(z) 2 time(z0) + I, 7. w; z; j=
UI
i there is a z1 such that (a) = z1
0, (b) time(z1) 2 time(z) + I, (c) w; z z1; 0 j= , (d) for all z2 6= z1 with z1 = z2 z3: w; z z2; z3 0 j= 8. w; z; j=
SI
i there is a z1 such that (a) z = z1 z2, (b) time(z) 2 time(z1) + I, (c) w; z1; z2 j= , (d) for all z3 6= hi with z2 = z3 z4: w; z1 z3; z4 j=
We shortly explain the intuitive meaning of the temporal operators:
XI is true i holds at the next state (i.e., after the next action), which must be within interval I.
VI is true i holds at the previous state (i.e., before the last action), which must be within interval I.
UI is true i there is a state in the future within interval I where is true, and in all states before that, must be true.
SI is true i there is a state in the past within interval I where is true, and in all states between that state and the current state, must be true.
Note that trace formulas are only interpreted over actual traces of the program . Thus, a formula X is true even if there is a possible action a that renders to be false, as long as a does not occur in . Therefore, there is no need for a distinct predicate actual (s) as used by [18].
De nition 15 (Satis ability). A situation formula is satis able i there is a world w such that w j= De nition 16 (Validity). A situation formula is valid i for any world w: w j= . We also write j= for a valid situation formula . A trace formula is valid i for any world w and any trace : w; hi; j= . We also write j= for a valid trace formula . 4
t -ESG and ESG In the following, we compare the rst-order fragment of ESG to t -ESG. To distinguish the semantics of ESG and t -ESG, we denote the respective semantics with a subscript whenever necessary, e.g., Zt-ESG denotes the nite traces of t -ESG. We assume a slightly di erent program transition semantics for ESG: For an action term a, we only allow the transition hz; ai !w hz p; nil i if w; z j= Poss(p); the program can only transition from action a to nil if action a is currently possible. Formally, we replace Rule 1 of the ESG program transition semantics by the following rule:
1. hz; ai !w hz p; nil i if p = jajzw and w; z j= Poss(p) This is similar to replacing each primitive action a in a program by Poss(a)?; a as done by [6]. Additionally, as time and now have a special meaning in t -ESG, we assume wlog that does not mention either of them. Apart from that, syntax and semantics of ESG are similar to t -ESG, but without constrained temporal operators (e.g., no XI , only the unconstrained variant X ), and without any past temporal operators (V and S ). We refer to [6, 5] for the full ESG syntax and semantics. also j=ESG Theorem 1. Let be a rst-order sentence of ESG that does not mention time or now . If j=t-ESG , then .
Proof. We show that if there is an ESG world w and an ESG trace z 2 ZESG with w; z 6j= , then there is a t-ESG world wt and a t-ESG trace zt 2 Zt-ESG with wt; zt 6j= .
Let w be an ESG world and z = ha1; : : : ; aki 2 ZESG such that w; z 6j= . We construct wt and zt with wt; zt j= i w; z j= as follows: Let wt be a t-ESG world such that for every 2 P and every zt0 = h(a01; t01) ; (a02; t02) ; : : : ; a0j; t0j i: wt[ ; h(a01; t01) ; (a02; t02) ; : : : ; a0j; t0j i]
= w[ ; ha01; a02; : : : ; a0ji] In other words, wt agrees with w on any primitive uent after any sequence of actions irrespective of the time. Additionally, we set zt = h(a1; 1) ; (a2; 2) ; : : : (ak; k)i. First, we need to show that jpjzw = jpjzwtt for any term p occurring in . We do this by induction over p: Let p 2 N . Then jpjzw = jpjzwtt = t.
Let p = f (p1; : : : ; pl).
Then, by de nition of j j, jpjzw = w[f (n1; : : : ; nl)z] with ni = jpijzw. By induction, jpijzwtt = jpijzw, and thus jpijzwtt = ni. Also, by de nition of wt, wt[f (n1; : : : ; nl); zt] = w[f (n1; : : : ; nl); z], and thus jpjzwtt = jpjzw.
Note that p cannot mention now because mention now .
Now, we show by induction over i w; z j= .
does not that wt; zt j= Let = F (p1; : : : ; pl). As shown: jpijzwtt = jpijzw. Therefore, by de nition of wt, wt[F (p1; : : : ; pl); zt] = w[F (p1; : : : ; pl); z], and thus wt; zt j= i w; z j= .
Let = (p1 = p2). With jpijzwtt = jpijzw, it follows that jp1jzwtt = jp2jzwtt i jp1jzw = jp2jzw, and thus wt; zt j= i w; z j= .
Let = ^ . By induction, wt; zt j= i w; z j= and wt; zt j= i w; z j= . As the semantics of the connective ^ do not di er between ESG and t-ESG, it follows that wt; zt j= i w; z j= . Let = : . By induction: wt; zt j= i w; z j= .
Let = 8x: . By induction, for each n 2 Nx: wt; zt j= nx i w; z j= nx. As ESG and t-ESG use the same standard names Nx, it follows that wt; zt j= i w; z j= .
Let = . Assume w; z 6j= . Then there is a z0 2 ZESG with w; z z0 6j= . Let z0 = ha01; : : : ; a0ji. Then, we set zt0 = h(a01; k + 1) ; : : : ; a0j; k + j i 2 Zt-ESG. By induction, wt; zt zt0 6j= .
For the other direction, assume wt; zt 6j= . Then there is zt0 = h(a01; k + 1) ; : : : ; a0j; k + j i 2 Zt-ESG with wt; zt zt0 6j= . By induction, it follows that for z0 = ha01; : : : ; a0ji: w; z z0 6j= : Therefore, w; z j= i wt; zt j= .
Let
= [ ] . First, note that k kzwtt = fh(a01; t01) ; (a02; t02) ; : : : ; a0j; t0j i j ha01; a02; : : : ; a0ji 2 k kzw; ti 2 NN ; t1
time(zt); for i < j : ti This follows from the fact that the program transition semantics k k di ers from ESG to t-ESG only in Rule 1, where we add a constraint on time. As does not mention now or time, the additional constraint only enforces monotonically non-decreasing time.
Now, assume there is z0 = ha01; : : : ; a0li 2 k kzw with w; z z0 6j= . Then zt0 = h(a01; t0) ; : : : ; (a0l; t0)i 2 k kzwtt with t0 = time(z). By induction, wt; zt zt0 6j= .
For the other direction, assume there is zt0 = h(a01; t01) ; : : : ; (a0l; t0l)i 2 k kzwtt with wt; zt zt0 6j= . Then z0 = ha1; : : : ; ali 2 k kzw and by induction: w; z z0 6j= . Thus, w; z j= [ ] i wt; zt j= [ ] . Let = J K . First, note that Equation 1 also holds for in nite traces.
Let 2 k kzw be an arbitrary trace with =
ha01; a02; : : :i, then t = h(a01; t01) ; (a02; t02) ; : : :i 2
k kzwtt for arbitrary ti with the constraints from
Equation 1. We show by sub-induction over :
w; z; j= i wt; zt; t j= .
(
There is p 2 PA with = p 0 such that w; z p; 0 j= . Then there is a tp time(zt) such that t = (p; tp) t0. By induction, wt; zt (p; tp) ; 0 j= . Furthermore, in t-ESG, X is short-hand for X[0;1) . As tp 2 time(zt) + [0; 1), it follows that wt; zt; t j= X .
Now, assume wt; zt; t j= X . There is p 2 NA with t = (p; tp) t0 such that tp time(zt) and wt; zt (p; tp) ; t0 j= . By Equation 1, there is a 0 = ha01; : : :i such that = p 0 and t0 = h(a01; t01) ; : : :i. Then, by induction: w; z p; 0 j= . { Let = 1 U 2. First, note that in t -ESG, U stands for U[0;1) , thus there are no constraints on the time. Similar to the previous case, we can construct pairs (zi; zt;i), such that w; z zi; 0 j= i wt; zt zt;i; t0 j= , same for . Thus, by induction, w; z; j=
U i wt; zt; t j= U .
Note that the other direction of the theorem is not true; a valid sentence in ESG is not necessarily valid in t -ESG. As an example, consider the sentence = [A]F _ [A]:F In ESG, is valid, because for each w, either w j= [A]F or w j= [A]:F , as w[F; hAi] is either 0 or 1. However, in t-ESG, is not valid. Consider a world wt of t -ESG with w[F; h(A; 0)i] = 0 and w[F; h(A; 1)i] = 1, i.e., if A is performed at time 0, then F is false, but if it is performed at time 1, then F is true. Thus, w 6j= [A]F , but also w 6j= [A]:F , and therefore w 6j= . 5 t -ESG and MTL We show that MTL is part of t -ESG. We do this by translating a timed word of MTL into an t -ESG world w. First, we summarize MTL and its pointwise semantics following the notation by [17].
De nition 17 (Formulas of MTL). Given a set P of atomic propositions, the formulas of MTL are built as follows: ::= p j : j ^ j
UI De nition 18 (Pointwise semantics of MTL). Given an alphabet of events , a timed word is a nite or in nite sequence ( 0; 0) ( 1; 1) : : : where i 2 and i 2 R+ such that the sequence ( i) is monotonically non-decreasing1 and non-Zeno.
Given a timed word = ( ; ) over alphabet 2P
and an MTL formula , ; i j= is de ned as usual
for the boolean operators, and with the following rule
for UI : ; i j= 1 UI 2 i there exists j such that
(
Theorem 2. Let be a sentence of MTL. Then j=t-ESG i j=MTL .
1Some variants of MTL require ( i) to be strictly increasing, which can be represented in t-ESG by requiring strictly increasing traces.
Proof. We assume wlog that P F 0, i.e., atomic propositions of MTL are 0-ary uents of t -ESG. Given a t -ESG world w and a trace , we construct a timed word such that w; hi; j=t-ESG i j=MTL , and vice versa. ): Let w be a t -ESG world and a trace. We construct the timed word = ( ; ) as follows: 1. Set 0 = 0 and 0[p] = w[p; hi] for every p 2 P . 2. For every i 2 N : For (i) = (ai; ti), set i = ti. 3. For every nite pre x zi = h(a1; t1) ; : : : ; (ai; ti)i of and every p 2 P , set i[p] = w[p; zi].
We show that w; zi; j=t-ESG over . i ; i j= by induction Let = pi be an atomic formula. The claim follows by de nition of .
Let = : . By induction, w; zi; j= , so the claim follows. i ; i j= Let = 1 ^ 2. By induction, w; zi; j= 1 i ; i j= 1, same for 2.
Let
= 1 UI 2.
First, assume w; zi; j= 1 UI 2. Then there is a zj with = zj 0 such that time(zj) 2 time(zi)+I, w; zi zj; 0 j= 2, and for all zk 6= zj with zj = zk zl: w; zi zk; zl 0 j= 1. Then, by de nition of : ; i + j j= 2, j 2 I, and for all k with i < i + k < i + j, ; i + k j= 1. Thus, by de nition of MTL's UI : ; i j= 1 UI 2.
Now, assume ; i j= 1 UI 2. Similar to the previous case: There is a j with i < j < j j, ; j j= 2, j i 2 I, and for all k with i < k < j: ; k j= 1. Then, by de nition of , there is a zj with = zj 0 and: w; zi zj; 0 j= 1. Furthermore, time(zi zj) 2 time(zi) + I, and for all zk 6= zj with zj = zk zl: w; zi zk; zl 0 j= 2.
Thus, w; zi; j= 1 UI 2. (: Given a timed word = ( ; ), we construct the world w and trace as follows: 1. (i) = (a; i) 2. w[p; hi] = 0[p] for every p 2 P 3. w[p; h(a; 1) ; (a; 2) ; : : : ; (a; i)i] = i[p] for every i 2 N and every p 2 P Analogously to above, we show that w; zi; j=t-ESG i ; i j= by induction over .
a,
Similarly to ES and ESG, a t -ESG BAT is a set of sentences describing the initial situation and the agent's actions with their preconditions and e ects. De nition 19 (Basic Action Theory). Given a set of uent predicates F , a set t -ESG of sentences is called a basic action theory over F i = 0 [ pre [ post, where mentions only uents in F and 0 is any set of uent sentences, pre is a set of uent formulas with free variable post is a set of sentences, with one sentence of the form [a]f (~x) f for each uent predicate f 2 F , and one sentence of the form [a]f (~x) = v f for each f 2 H [ I, and where f is a uent formula.
In a BAT, 0 describes the initial situation, post is a set of successor state axioms, and pre is a set of precondition axiom for all actions in the domain that is understood disjunctively, i.e., from pre, we construct a single precondition axiom of the form Poss(a) W pre. This is slightly di erent to ES and ESG and allows us to combine multiple basic action theories. 6.1
A Simple Carrier Robot We present a BAT of a simple robot that can move around and pick up and put down objects. All actions are modeled as durative actions with start and stop actions.
pre = f 9s; g: a = start goto(s; g)
^ :9a0: Performing (a0); 9s; g: a = end goto(s; g)^
now
time(goto(s; g)) + d (s; g); g 9o; l: a = start pick (o)^
RobotAt (l) ^ At (o; l); 9o: a = end pick (o)^ Performing (pick(o))^ now
time(pick (o)) + 3; 9o; l: a = start put (o; l)^
9o; l: a = end put (o; l)^
Performing (put(o; l))^
now
time(put (o; l)) + 2
(
The precondition axiom states that the robot can
(
The robot's actions have e ects on the following
predicates:
The successor state axioms state that (
As usual in Golog, we de ne while and if then else as macros: while do
done d=ef ( ?; ) ; : ? if then 1 else 2
d=ef [ ?; 1] j [: ?; 2] if then 1 d=ef if then 1 else nil
The BAT already allows us to de ne simple Golog a simpli ed version may look as follows:
M pre = f a = start calibration^ state(arm) 6= calibrating ^ state(arm) 6= calibrated ; a = end calibration^ time(start calibration) state(arm) = calibrating ; 5 ^ a = start perception^
state(perception) 6= running a = stop perception^
state(perception) = running g programs. The program shown in Listing 1 picks up all objects from the table and puts them onto the shelf.
0 = fRobotAt (shelf );
At (obj1 ; table); At (obj3 ; shelf ); d(shelf ; table) = 20; d(table; shelf ) = 20; 8o: (o 6= obj1 ^ o 6= obj3 ) :9l: At (o; l)g
j= [ ]:9o: At (o; table) j= [ ]RobotAt (table)
Following the program transition semantics, one possible successful trace of is: z = h (start goto(table); 0) ; (end goto(table); 20) ; (start pick (obj1 ); 20) ; (end pick (obj1); 23) ; (start goto(shelf ); 23) ; (end goto(shelf ); 43) ; (start put (obj1 ); 43) ; (end put (obj1); 45)i 7
Listing 1 already shows an abstract program that clears
the table. However, to execute the program on a real
robot, additional constraints must be satis ed, e.g.,
the robot's perception module needs to be enabled
before an object is picked up or put down. Instead
of encoding this in the abstract BAT, we provide an
additional maintenance BAT which takes care of these
kinds of constraints. Such a maintenance BAT may be
generated from platform models as shown in Figure 1,
(
state(perception) = paused g
Using the maintenance BAT, we can formulate a set of additional constraints that must be satis ed during the execution of any program :
J KG 9o: Performing (pick (o))
state(arm) = calibrated J KG 9o; l: Performing (put (o; l))
state(arm) = calibrated J KG 9o: Performing (pick (o))
H 1 state(perception) = running J KG :F 1 9o; l:(Performing (pick (o))
_ Performing (put (o; l))) state(perception) = paused ) arm must be calibrated, (20) if the robot is performing a pick action, then the perception must have been running for at least 1 second, (21) if the robot is not performing a pick or put action in the next second, then the perception should be paused.
start start goto(table) As constraint language, we allow a subset of t -ESG. De nition 20 (Constraint). Given a BAT and a maintenance BAT M . Let be a uent trace formula only mentioning terms from . Let be a uent trace formula only mentioning terms from M . Then the formula = is a constraint formula.
Intuitively, we interpret a constraint as follows: As is from the abstract BAT and we can only add actions from M to our action sequence, is given. Therefore, if is true, we need to add maintenance actions such that is also satis ed. In other words, we cannot satisfy a constraint by making false. De nition 21 (Constraint Satisfaction). Given a program and a BAT , we say that a constraint is satis ed by i
j= J KG 7.2
Solving Timed Temporal Constraints Using the example above, we now sketch a procedure that modi es a given action sequence of an abstract program to also satisfy the platform constraints. First, we convert the action sequence into a STN, where each action of the sequence is a node in the STN. Such a STN for the program in Listing 1 is shown in Figure 2.
For each node starting at the start node, we now check whether each constraint is satis ed. As an start start goto(table) example, in the node start pick (o1), Constraint 18 is not satis ed. From the platform models, we can generate an action sequence that satis es the constraint. In our example, by searching the state automaton in Figure 1, we can generate the sequence hstart calibrate; end calibratei, which is then added to the STN. Similarly, the perception needs to be running before doing a pick. Thus, the action start perception is added to the STN. By Constraint 20, the perception must have been running for at least 1 second. Thus, the edge from start perception to start pick (o1) has the time constraint [1; 1]. The resulting STN after checking all STN nodes and all constraints is shown in Figure 3. 8
We presented t -ESG, a logic for reasoning about actions that allows the speci cation of metric temporal constraints. t -ESG extends ESG with metric time and temporal operators referring to the past. We showed that Metric Temporal Logic (MTL) can be embedded into t -ESG, while ESG cannot be fully embedded into t -ESG.We presented a constraint language for specifying metric temporal constraints on a platform model, and we sketched a translation of those constraints into Simple Temporal Networks (STNs). Using the solution of the STN, the abstract Golog program can be transformed into an action sequence that is executable on the robot platform, thereby allowing the separation of the abstract agent behavior speci cation and the details of the platform, even if they are inter-dependent.
T. Hofmann was supported by the German National Science Foundation (DFG) under grant number GL747/23-1.