A Logic for Specifying Metric Temporal Constraints for Golog Programs Till Hofmann Gerhard Lakemeyer hofmann@kbsg.rwth-aachen.de gerhard@kbsg.rwth-aachen.de Knowledge-Based Systems Group RWTH Aachen University, Germany add respective actions to their programs, e.g., they can enable the perception before a pick action and Abstract disable it afterwards again. However, this makes the behavior specification much more complex and error- Executing a Golog program on an actual prone. If the program involves some form of planning robot typically requires additional platform or search, the platform details may cause performance constraints to be satisfied. Such constraints degradation, as the search space’s size is increased by are often temporal, refer to metric time, and the additional actions. Additionally, most of these plat- require modifications to the abstract Golog form details are not specific to one particular program, program. Based on ES and ESG, modal vari- but to the platform. Any change to the platform needs ants of the Situation Calculus, we propose the to be reflected in the behavior specification. As an logic t-ESG, a logic which allows the specifica- alternative, the developers may decide to use Golog tion of metric temporal constraints for Golog for an abstract behavior specification and deal with programs. We provide a comparison to ESG the platform details on the lower levels. However, this and show that Metric Temporal Logic (MTL) is often not possible, as platform constraints require can be embedded into t-ESG. We show how changes to the high-level program, and thus the pro- to formulate constraints using a model of the gram cannot be clearly separated from the platform it robot platform, and we sketch a procedure that is running on. solves those constraints using Simple Temporal In this paper, we propose a different approach: As Networks (STNs). before, the agent’s behavior is specified with an abstract program. However, based on platform models as shown 1 Introduction in Figure 1, we construct a maintenance BAT that While Golog [14], an agent programming language allows to specify a set of additional constraints on the based on the Situation Calculus [15, 20], allows a clear platform. The abstract plan from the original Golog and abstract specification of an agent’s behavior, exe- program is then transformed into an executable action cuting a Golog program on a real robot often creates sequence that satisfies the platform constraints. additional issues. Typically, the robot’s platform re- The main ideas of this approach were sketched in quires additional constraints that are ignored when [10]. In the following, we focus on the logical founda- designing a Golog program. As an example, a robot tions that allow the specification of metric temporal needs to calibrate its arm before it can use it, and it constraints. Our starting point is the logic ESG [6], a needs to enable its perception module before it inter- temporal variant of ES [13], which in turn is a modal acts with its environment. Developers typically face variant of the Situation Calculus. We extend ESG by two options: First, they can directly model all the metric time, quantitative temporal operators similar platform details in the basic action theory (BAT) and to Metric Temporal Logic (MTL) [12], and additional temporal operators previous and since, which refer to Copyright c by the paper’s authors. Copying permitted for private and academic purposes. past states in the same way as next and until refer to In: G. Steinbauer, A. Ferrein (eds.): Proceedings of the 11th future states. We show the relationship between ESG International Workshop on Cognitive Robotics, Tempe, AZ, USA, and t-ESG and we provide an embedding of MTL into 27-Oct-2018, published at http://ceur-ws.org t-ESG. Next, we show how to describe a BAT and an 36 Uncalibrated current situation by adding axioms for a distinct pred- start calibrate() icate actual , where actual (s) is true iff s is an actual 5s park() evolvement of the world. This differentiation is impor- Off Calibrating Calibrated Parked tant, because otherwise, we could not express much [0, 10]s move() about the future; as long as there is a possible action Error that causes a formula α to be false, we cannot state Busy move() that α is true in the next situation, even if the agent has no intention (e.g., it is not the next action in the Figure 1: A finite state machine as a platform model Golog program) to execute the action. As we will see, for the arm. The edges are annotated with their action this problem does not occur in ESG or t-ESG. and time bounds. Adapted from [10]. MTL [12] is an extension of Linear Time Logic (LTL) with metric time, which allows expressions such as F≤c , abstract Golog program in t-ESG and how to formu- meaning eventually within time c. In MTL, formulas late metric temporal platform constraints with t-ESG. are interpreted over timed words or timed state se- Finally, we sketch how to resolve those constraints with quences, where each state specifies which propositions a Simple Temporal Network (STN) to transform the are true, and each state has an associated time value. abstract program into an executable action sequence. Depending on the choice of the state and time theory, the satisfiability problem for MTL becomes undecid- 2 Foundations & Related Work able [2]. However, for finite words, it has been shown to be decidable [16]. MTL has been restricted to Metric The Situation Calculus [15, 20] is a first-order logic Interval Temporal Logic (MITL) [3], which prohibits for representing and reasoning about actions. Action singular intervals and is interpreted over time intervals preconditions and effects are axiomatized with basic instead of time points, which makes the satisfiability action theories and situations are histories of actions, problem for MITL decidable. MTLP [4] is an extension e.g., the situation term do(pick (o1), S0 ) refers to the of MTL with temporal operators referring to the past, situation after doing action pick (o1) in the initial situa- e.g., V (preVious) and S (Since). tion. The programming language Golog [14] is based on the Situation Calculus and offers imperative pro- Simple Temporal Networks (STNs) [8] provide an gramming constructs such as sequences of actions and efficient procedure to solve a constraint problem given iteration as well as non-deterministic branching and by a set of time-points {ti } and a set of binary temporal non-deterministic choice. The semantics of Golog constraints of the form tj − ti ≤ δ. Disjunctive Linear and its on-line variant IndiGolog can be specified in Relations (DLRs) [11] allow more expressive temporal terms of transitions [7]. constraints; the restricted Horn DLRs can be solved in The logic ES [13] is a modal variant of the Situa- polynomial time and still subsume STNs. tion Calculus which gets rid of explicit action terms Similar to the proposed approach, Schiffer, Wort- and uses modal operators instead. As an example, mann, and Lakemeyer extend Golog for self- [pick (o1)]Holding(o1) is satisfied iff Holding(o1) is true maintenance [21] by allowing temporal constraints us- after doing pick (o1). The logic ESG [6, 5] is a temporal ing Allen’s Interval Algebra [1]. Those constraints are extension of ES for the verification of Golog programs. resolved on-line by interleaving the original program It specifies program transition semantics similar to the with maintenance actions. Closely related is also the transition semantics of IndiGolog and extends ES work by [9], who propose a hybrid approach of temporal with the temporal operators X (next) and U (until ). constraint reasoning and reasoning about actions based The Situation Calculus has also been extended by a on the Situation Calculus. Similar to [21], they allow notion of time. Reiter requires each action A to have an constraints based on Allen’s Interval Algebra, which explicit time argument, i.e., each action is of the form are translated into a temporal constraint network. 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., 3 Timed ESG do({end pick (o1), start goto(kitchen)}, s) refers to the situation after ending the action pick (o1) and at the In this section, we present the syntax and semantics same time start moving to the kitchen. A similar ap- of t-ESG. As t-ESG is based on ESG, its syntax and proach is described by [18], which also allows temporal semantics are also based on ESG and ES. We refer to reasoning about situations. In particular, they differ- [13, 6, 5] for more details on the original syntax and entiate between possible and actual evolvements of the semantics. 37 3.1 Syntax Definition 3 (Programs). Definition 1 (Language of t-ESG). The language con- δ ::= t | α? | δ1 ; δ2 | δ1 |δ2 | πx. δ | δ1 kδ2 | δ ∗ sists of formulas over symbols from the following vo- cabulary: where t is an action term and α is a static situation formula. A program consists of primitive actions t, tests 1. object variables x1 , x2 , x3 , . . . , y1 , . . . α?, sequences δ1 ; δ2 , nondeterministic branching δ1 |δ2 , 2. action variables a, a1 , a2 , a3 , . . . nondeterministic choice of argument πx. δ, interleaved concurrency δ1 kδ2 , and nondeterministic iteration δ ∗ . 3. number variables t1 , t2 , t3 , . . . Definition 4 (Situation Formulas). The situation for- 4. object standard names NO = {o1 , o2 , o3 , . . .} mulas are the least set such that 5. action standard names NA = {p1 , p2 , p3 , . . .} 1. if t1 , . . . , tk are terms and P is a k-ary predicate symbol, then P (t1 , . . . , tk ) is a situation formula, 6. number standard names NN = {0, 1, 2, 12 , . . .}; here, we assume NN = Q 2. if t1 and t2 are terms, then (t1 = t2 ) is a situation 7. fluent predicates of arity k: F : k {f1k , f2k , . . .}, formula, e.g., Holding; we assume this list contains the 3. if α and β are situation formulas, x is a variable, distinguished predicates Poss and < P is a predicate symbol, δ is a program, and φ is 8. rigid functions of arity k: G k = {g1k , g2k , . . .}, e.g., a trace formula, then α ∧ β, ¬α, ∀x. α, α, [δ]α, goto; including distinguished functions +, · ∈ G2 and JδKφ are situation formulas. 9. fluent object functions of arity k: Hk = We call a situation formula of the form P (n1 , . . . , nk ) {hk1 , hk2 , . . .}, e.g., parent with ni ∈ N a primitive formula and denote the set of primitive formulas as PF . 10. fluent number functions of arity k: I k = {ik1 , ik2 , . . .}, e.g., battery; including distinguished Definition 5 (Trace Formulas). The trace formulas functions time ∈ I 1 and now ∈ I 0 are the least set such that 11. open, closed, and half-closed intervals, e.g., [1, 2], 1. if α is a situation formula, then it is also a trace with constants of sort number as interval endpoints formula, 12. connectives and other symbols: =, ∧, ∨, ¬, ∀, 2. if φ and ψ are trace formulas, x is a variable, and XI ,VI , UI , SI (with interval I), , [·], J·K I is an interval, then φ ∧ ψ, ¬φ, ∀x. φ, XI φ, VI φ, φ SI ψ, and φ UI ψ are also trace formulas. We also write F for the set k∈N0 F k , similarly for S G, H, I. We also denote the set of standard names as We also write < c, ≤ c, = c, > c, and ≥ c for the N = NO ∪ NA ∪ NN . Furthermore, we call a term respective intervals [0, c), [0, c], [c, c], (c, ∞), and [c, ∞). def primitive if it is of the form f (n1 , . . . , nk ), with f, ni We use the short-hand notation FI φ = (> UI φ) being standard names. We denote the set of primitive def (future) and GI φ = ¬FI ¬φ (globally), as well as terms as PO (objects), PA (actions), and PN (numbers), def def and P = PO ∪ PA ∪ PN . PI φ = (> UI φ) (past) and HI φ = ¬PI ¬φ (his- We read XI as next (within interval I), VI as torically). For intervals, c + [s, e] denotes the interval previously (within interval I), UI as until (within [s+c, e+c], similarly for c+(s, e), c+[s, e), and c+(s, e]. interval I), and SI as since (within interval I). We also omit the interval I if I = [0, ∞), e.g., φ U ψ is short for φ U[0,∞) ψ. Definition 2 (Terms of t-ESG). The set of terms of t-ESG is the least set such that Definition 6 (Static Formulas). A situation formula α is static if it contains no [·], , or J·K operators. • every variable is a term of the corresponding sort, Definition 7 (Bounded Formulas). A situation for- • every standard name is a term of the corresponding mula α is bounded if it contains no  or J·K operators, sort, and [t] operators only in case the argument is an atomic action t. • if t1 , . . . , tk are terms and f is a k-ary function symbol, then f (t1 , . . . , tk ) is a term of the same Definition 8 (Fluent Formulas). A situation formula sort as f . α is fluent if it is static and contains no predicate Poss. 38 3.1.1 Comparison to ESG 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 The language of t-ESG extends the language of ESG never occurred. by the constrained temporal operators XI and UI . Also, ESG has no operators referring to the past; i.e., Definition 12 (Program Transition Semantics). The no V or S (or their constrained variants VI and SI ). w transition relation → among configurations, given a Finally, as we understand X φ (φ U ψ) as short-hand world w, is the least set satisfying notation for X[0,∞) φ (φ U[0,∞) ψ), the language of ESG w is a subset of t-ESG. 1. hz, ai → hz · (p, t) , nil i, if p = |a|zw , t ≥ time(z), and w, z · (nil , t) |= Poss(p) 3.2 Semantics w w 2. hz, δ1 ; δ2 i → hz · p, γ; δ2 i, if hz, δ1 i → hz · p, γi, Definition 9 (Timed Traces). A timed trace is a pos- w w sibly infinite timed sequence of action standard names 3. hz, δ1 ; δ2 i → hz · p, δ 0 i if hz, δ1 i ∈ F w and hz, δ2 i → with monotonically non-decreasing time. Formally, a hz · p, δ 0 i trace π is a mapping π : N → PA × NN , and for any w w i, j ∈ N with π(i) = (σi , ti ), π(j) = (σj , tj ) : If i < j, 4. hz, δ1 |δ2 i → hz · p, δ 0 i if hz, δ1 i → hz · p, δ 0 i or w then ti ≤ tj . Also, we require the sequence (ti )i∈N to hz, δ2 i → hz · p, δ 0 i be non-Zeno, i.e., it is either finite or unbounded. w w 5. hz, πx. δi → hz · p, δ 0 i, if hz, δnx i → hz · p, δ 0 i for For a finite timed trace z = h(a1 , t1 ) · (a2 , t2 ) · . . . · some n ∈ Nx def w w (ak , tk )i, we define time(z) = tk , i.e., time(z) is the 6. hz, δ ∗ i → hz · p, γ; δ ∗ i if hz, δi → hz · p, γi time value of the last action in z. We denote the set of w w finite timed traces as Z, the set of infinite timed traces 7. hz, δ1 kδ2 i → hz · p, δ 0 kδ2 i if z, δ1 → hz · p, δ 0 i as Π, and the set of all traces as T = Z ∪ Π. w w 8. hz, δ1 kδ2 i → hz · p, δ1 kδ 0 i if z, δ2 → hz · p, δ 0 i Definition 10 (World). Intuitively, a world w deter- mines the truth of fluent predicates as well as the The set of final configurations F w is the smallest set value of fluent functions, not just initially, but after such that any (timed) sequence of actions. Formally, a world 1. hz, α?i ∈ F w if w, z |= α, is a mapping w that maps (1) PF × Z → {0, 1}, (2) PO × Z → NO , and (3) PN × Z → NN . 2. hz, δ1 ; δ2 i ∈ F w if hz, δ1 i ∈ F w and hz, δ2 i ∈ F w Similar to ES and ESG, the truth of a fluent after 3. hz, δ1 |δ2 i ∈ F w if hz, δ1 i ∈ F w , or hz, δ2 i ∈ F w any sequence of actions is determined by a world w. 4. hz, πx. δi ∈ F w if hz, δnx i ∈ F w for some n ∈ Nx Different to ES and ESG, we require all traces referred by a world to contain time values for each action. This 5. hz, δ ∗ i ∈ F w also means that in the same world, a fluent predicate F (~n) may have a different value after the same sequence 6. hz, δ1 kδ2 i ∈ F w if hz, δ1 i ∈ F w and hz, δ2 i ∈ F w of actions if the actions were executed at different times, The program transition semantics is very similar to i.e., w[F (~n, h(a1 , 1)i] may have a different value than the semantics of ESG. The only difference is in Rule 1, w[F (~n, h(a1 , 2)i]. which has an additional constraint on the time, and Definition 11 (Denotation of terms). Given a ground which requires the action to be executable. term t, a world w, and a timed trace z ∈ Z, we define Definition 13 (Program Traces). Given a world w |t|zw by: and a finite sequence of action standard names z, the 1. if t ∈ N , then |t|zw = t, set kδkzw of (timed) traces of a program δ is 2. if t = now , then |t|zw = time(z), kδkzw = w∗ 3. if t = time(a(t1 , . . . , tk )), then |t|zw = max {ta | {z 0 ∈ Z | hz, δi → hz · z 0 , δ 0 i and hz · z 0 , δ 0 i ∈ F w }∪ w w w (a(n1 , . . . , nk ), ta ) ∈ z} ∪ {0}, where ni = |ti |zw , {π ∈ Π | hz, δi → hz · π (1) , δ1 i → hz · π (2) , δ2 i → . . . 4. if t = f (t1 , . . . , tk ) then |t|zw = w[f (n1 , . . . , nk ), z], where for all i ≤ 0, hz · π (i) , δi i ∈ / F w} where ni = |ti |zw Definition 14 (Truth of Situation and Trace Formu- Note the special denotation for the function symbols las). Given a world w ∈ W and a situation formula α, now ∈ I0 and time ∈ I1 . The term now always refers we define w |= α as w, hi |= α, where for any z ∈ Z: 39 1. w, z |= F (t1 , . . . , tk ) iff w[F (n1 , . . . , nk ), z] = 1, • VI φ is true iff φ holds at the previous state (i.e., where ni = |ti |zw , before the last action), which must be within in- terval I. 2. w, z |= (t1 = t2 ) iff n1 and n2 are identical, where ni = |ti |zw , • φ UI ψ is true iff there is a state in the future within interval I where ψ is true, and in all states 3. w, z |= α ∧ β iff w, z |= α and w, z |= β before that, φ must be true. 4. w, z |= ¬α iff w, z 6|= α • φ SI ψ is true iff there is a state in the past within interval I where ψ is true, and in all states between 5. w, z |= ∀x. α iff w, z |= αnx for all n ∈ Nx that state and the current state, φ must be true. 6. w, z |= α iff w, z · z 0 |= α for all z 0 ∈ Z Note that trace formulas are only interpreted over 7. w, z |= [δ]α iff for all finite z 0 ∈ kδkzw , w, z · z 0 |= α actual traces of the program δ. Thus, a formula X α is true even if there is a possible action a that renders α 8. w, z |= JδKφ iff for all τ ∈ kδkzw , w, z, τ |= φ to be false, as long as a does not occur in δ. Therefore, there is no need for a distinct predicate actual (s) as Intuitively, [δ]α means that after every execution of δ, used by [18]. the situation formula α is true. JδKφ means that during every execution of δ, the trace formula φ is true. Definition 15 (Satisfiability). A situation formula α The truth of trace formulas φ is defined as follows is satisfiable iff there is a world w such that for w ∈ W, z ∈ Z, and τ ∈ T : w |= α 1. w, z, τ |= α iff w, z |= α and α is a situation Definition 16 (Validity). A situation formula α is formula, valid iff for any world w: w |= α. We also write |= α 2. w, z, τ |= φ ∧ ψ iff w, z, τ |= φ and w, z, τ |= ψ, for a valid situation formula α. A trace formula φ is valid iff for any world w and any trace τ : w, hi, τ |= φ. 3. w, z, τ |= ¬φ iff w, z, τ 6|= φ, We also write |= φ for a valid trace formula φ. 4. w, z, τ |= ∀x. φ iff w, z, τ |= φxn for all n ∈ Nx , 4 t-ESG and ESG 0 5. w, z, τ |= XI φ iff there is p ∈ PA with τ = p · τ , In the following, we compare the first-order fragment w, z · p, τ 0 |= φ, and time(p) ∈ time(z) + I, of ESG to t-ESG. To distinguish the semantics of ESG and t-ESG, we denote the respective semantics with a 6. w, z, τ |= VI φ iff z = z 0 · p for some p ∈ PA , subscript whenever necessary, e.g., Zt-ESG denotes the w, z 0 , p · τ |= φ, and time(z) ∈ time(z 0 ) + I, finite traces of t-ESG. We assume a slightly different 7. w, z, τ |= φ UI ψ iff there is a z1 such that program transition semantics for ESG: For an action w term a, we only allow the transition hz, ai → hz · p, nil i (a) τ = z1 · τ 0 , if w, z |= Poss(p); the program can only transition from (b) time(z1 ) ∈ time(z) + I, action a to nil if action a is currently possible. For- mally, we replace Rule 1 of the ESG program transition (c) w, z · z1 , τ 0 |= ψ, semantics by the following rule: (d) for all z2 6= z1 with z1 = z2 · z3 : w, z · z2 , z3 · w τ 0 |= φ 1. hz, ai → hz · p, nil i if p = |a|zw and w, z |= Poss(p) This is similar to replacing each primitive action a in a 8. w, z, τ |= φ SI ψ iff there is a z1 such that program δ by Poss(a)?; a as done by [6]. Additionally, (a) z = z1 · z2 , as time and now have a special meaning in t-ESG, we assume wlog that α does not mention either of them. (b) time(z) ∈ time(z1 ) + I, Apart from that, syntax and semantics of ESG are (c) w, z1 , z2 · τ |= ψ, similar to t-ESG, but without constrained temporal 6 hi with z2 = z3 · z4 : w, z1 · z3 , z4 · (d) for all z3 = 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 We shortly explain the intuitive meaning of the semantics. temporal operators: Theorem 1. Let α be a first-order sentence of ESG • XI φ is true iff φ holds at the next state (i.e., after that does not mention time or now . If |=t-ESG α, then the next action), which must be within interval I. also |=ESG α. 40 Proof. We show that if there is an ESG world w and For the other direction, assume wt , zt 6|= α. an ESG trace z ∈ ZESG with w, z 6|= α, then there is Then there is zt0 = h(a01 , k + 1) , . . . , a0j , k + j i ∈ a t-ESG world wt and a t-ESG trace zt ∈ Zt-ESG with Zt-ESG with wt , zt · zt0 6|= β. By induction, it follows wt , zt 6|= α. that for z 0 = ha01 , . . . , a0j i: w, z · z 0 6|= β. Let w be an ESG world and z = ha1 , . . . , ak i ∈ ZESG Therefore, w, z |= β iff wt , zt |= β. such that w, z 6|= α. We construct wt and zt with wt , zt |= α iff w, z |= α as follows: Let wt be a • Let α = [δ]β. First, note that t-ESG world such that for every  ρ ∈ P and every kδkzwtt = {h(a01 , t01 ) , (a02 , t02 ) , . . . , a0j , t0j i |  (1) zt0 = h(a01 , t01 ) , (a02 , t02 ) , . . . , a0j , t0j i: ha01 , a02 , . . . , a0j i ∈ kδkzw , wt [ρ, h(a01 , t01 ) , (a02 , t02 ) , . . . , a0j , t0j i]  ti ∈ NN , t1 ≥ time(zt ), for i < j : ti ≤ tj } = w[ρ, ha01 , a02 , . . . , a0j i] This follows from the fact that the program transi- In other words, wt agrees with w on any primitive fluent tion semantics k · k differs from ESG to t-ESG only after any sequence of actions irrespective of the time. in Rule 1, where we add a constraint on time. As α Additionally, we set zt = h(a1 , 1) , (a2 , 2) , . . . (ak , k)i. does not mention now or time, the additional con- First, we need to show that |p|zw = |p|zwtt for any term straint only enforces monotonically non-decreasing p occurring in α. We do this by induction over p: time. Now, assume there is z 0 = ha01 , . . . , a0l i ∈ kδkzw with • Let p ∈ N . Then |p|zw = |p|zwtt = t. w, z · z 0 6|= β. Then zt0 = h(a01 , t0 ) , . . . , (a0l , t0 )i ∈ • Let p = f (p1 , . . . , pl ). kδkzwtt with t0 = time(z). By induction, wt , zt ·zt0 6|= Then, by definition of | · |, |p|zw = w[f (n1 , . . . , nl )z] β. with ni = |pi |zw . By induction, |pi |zwtt = |pi |zw , For the other direction, assume there is zt0 = and thus |pi |zwtt = ni . Also, by definition of h(a01 , t01 ) , . . . , (a0l , t0l )i ∈ kδkzwtt with wt , zt · zt0 6|= β. wt , wt [f (n1 , . . . , nl ), zt ] = w[f (n1 , . . . , nl ), z], and Then z 0 = ha1 , . . . , al i ∈ kδkzw and by induction: thus |p|zwtt = |p|zw . w, z · z 0 6|= β. Thus, w, z |= [δ]β iff wt , zt |= [δ]β. Note that p cannot mention now because α does not • Let α = JδKβ. First, note that Equation 1 also mention now . holds for infinite traces. Now, we show by induction over α that wt , zt |= α Let τ ∈ kδkzw be an arbitrary trace with τ = iff w, z |= α. ha01 , a02 , . . .i, then τt = h(a01 , t01 ) , (a02 , t02 ) , . . .i ∈ kδkzwtt for arbitrary ti with the constraints from • Let α = F (p1 , . . . , pl ). As shown: Equation 1. We show by sub-induction over φ: |pi |zwtt = |pi |zw . Therefore, by definition of w, z, τ |= φ iff wt , zt , τt |= φ. wt , wt [F (p1 , . . . , pl ), zt ] = w[F (p1 , . . . , pl ), z], and thus wt , zt |= α iff w, z |= α. – Let φ = β be a situation formula. Then by induction: w, z |= β iff wt , zt |= β. • Let α = (p1 = p2 ). With |pi |zwtt = |pi |zw , it follows that |p1 |zwtt = |p2 |zwtt iff |p1 |zw = |p2 |zw , and thus – Let φ = φ1 ∧ φ2 . As in the case for the situa- wt , zt |= α iff w, z |= α. tion formula, the semantics of the connective ∧ do not differ between ESG and t-ESG. • Let α = β ∧ γ. By induction, wt , zt |= β iff w, z |= – Let φ = ¬ψ. By sub-induction: w, z, τ |= ψ β and wt , zt |= γ iff w, z |= γ. As the semantics of iff wt , zt , τt |= ψ. the connective ∧ do not differ between ESG and t-ESG, it follows that wt , zt |= α iff w, z |= α. – Let φ = ∀x. ψ. Again, as ESG and t-ESG use the same standard names, we can fol- • Let α = ¬β. By induction: wt , zt |= β iff w, z |= β. low by sub-induction: Nx , w, z, τ |= ψnx iff wt , zt , τt |= ψnx for every n ∈ Nx . • Let α = ∀x. α. By induction, for each n ∈ Nx : wt , zt |= αnx iff w, z |= αnx . As ESG and t-ESG – Let φ = X ψ. Assume w, z, τ |= X ψ. use the same standard names Nx , it follows that There is p ∈ PA with τ = p · τ 0 such wt , zt |= α iff w, z |= α. that w, z · p, τ 0 |= ψ. Then there is a tp ≥ time(zt ) such that τt = (p, tp ) · τt0 . By • Let α = β. Assume w, z 6|= α. Then there is a induction, wt , zt · (p, tp ) , τ 0 |= ψ. Further- z 0 ∈ ZESG with w, z · z 0 6|= β. Let z 0 = ha01 , . . . , a0j i. more, in t-ESG, X is short-hand for X[0,∞) . Then, we set zt0 = h(a01 , k + 1) , . . . , a0j , k + j i ∈  As tp ∈ time(zt ) + [0, ∞), it follows that Zt-ESG . By induction, wt , zt · zt0 6|= β. wt , zt , τt |= X ψ. 41 Now, assume wt , zt , τt |= X ψ. There is Proof. We assume wlog that P ⊆ F 0 , i.e., atomic p ∈ NA with τt = (p, tp ) · τt0 such that propositions of MTL are 0-ary fluents of t-ESG. Given tp ≥ time(zt ) and wt , zt · (p, tp ) , τt0 |= ψ. By a t-ESG world w and a trace π, we construct a timed Equation 1, there is a τ 0 = ha01 , . . .i such that word ρ such that w, hi, π |=t-ESG φ iff ρ |=MTL φ, and τ = p · τ 0 and τt0 = h(a01 , t01 ) , . . .i. Then, by vice versa. induction: w, z · p, τ 0 |= ψ. ⇒: Let w be a t-ESG world and π a trace. We construct – Let φ = ψ1 U ψ2 . First, note that in t-ESG, the timed word ρ = (σ, τ ) as follows: U stands for U[0,∞) , thus there are no con- straints on the time. Similar to the previous 1. Set τ0 = 0 and σ0 [p] = w[p, hi] for every p ∈ P . case, we can construct pairs (zi , zt,i ), such 2. For every i ∈ N : For π(i) = (ai , ti ), set τi = ti . that w, z · zi , τ 0 |= ψ iff wt , zt · zt,i , τt0 |= ψ, same for φ. Thus, by induction, w, z, τ |= 3. For every finite prefix zi = h(a1 , t1 ) , . . . , (ai , ti )i φ U ψ iff wt , zt , τt |= φ U ψ. of π and every p ∈ P , set σi [p] = w[p, zi ]. Note that the other direction of the theorem is not true; a valid sentence in ESG is not necessarily valid in We show that w, zi , π |=t-ESG φ iff ρ, i |= φ by induction t-ESG. As an example, consider the sentence over φ. α = [A]F ∨ [A]¬F • Let φ = pi be an atomic formula. The claim follows by definition of ρ. In ESG, α is valid, because for each w, either w |= [A]F or w |= [A]¬F , as w[F, hAi] is either 0 or 1. However, • Let φ = ¬ψ. By induction, w, zi , π |= ψ iff ρ, i |= in t-ESG, α is not valid. Consider a world wt of t-ESG ψ, so the claim follows. 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 • Let φ = φ1 ∧ φ2 . By induction, w, zi , π |= φ1 iff performed at time 1, then F is true. Thus, w 6|= [A]F , ρ, i |= φ1 , same for φ2 . but also w 6|= [A]¬F , and therefore w 6|= α. • Let φ = φ1 UI φ2 . 5 t-ESG and MTL First, assume w, zi , π |= φ1 UI φ2 . Then there is a We show that MTL is part of t-ESG. We do this by zj with π = zj ·π 0 such that time(zj ) ∈ time(zi )+I, translating a timed word ρ of MTL into an t-ESG world w, zi · zj , π 0 |= φ2 , and for all zk 6= zj with zj = w. First, we summarize MTL and its pointwise seman- zk · zl : w, zi · zk , zl · π 0 |= φ1 . Then, by definition tics following the notation by [17]. of ρ: ρ, i + j |= φ2 , τj ∈ I, and for all k with i < i + k < i + j, ρ, i + k |= φ1 . Thus, by definition Definition 17 (Formulas of MTL). Given a set P of of MTL’s UI : ρ, i |= φ1 UI φ2 . atomic propositions, the formulas of MTL are built as Now, assume ρ, i |= φ1 UI φ2 . Similar to the follows: previous case: There is a j with i < j < |ρ|, φ ::= p | ¬φ | φ ∧ φ | φ UI φ ρ, j |= φ2 , τj − τi ∈ I, and for all k with i < k < j: ρ, k |= φ1 . Then, by definition of ρ, there is a Definition 18 (Pointwise semantics of MTL). Given zj with π = zj · π 0 and: w, zi · zj , π 0 |= φ1 . Fur- an alphabet of events Σ, a timed word ρ is a finite or thermore, time(zi · zj ) ∈ time(zi ) + I, and for all infinite sequence (σ0 , τ0 ) (σ1 , τ1 ) . . . where σi ∈ Σ and zk 6= zj with zj = zk · zl : w, zi · zk , zl · π 0 |= φ2 . τi ∈ R+ such that the sequence (τi ) is monotonically Thus, w, zi , π |= φ1 UI φ2 . non-decreasing1 and non-Zeno. Given a timed word ρ = (σ, τ ) over alphabet 2P ⇐: Given a timed word ρ = (σ, τ ), we construct the and an MTL formula φ, ρ, i |= φ is defined as usual world w and trace π as follows: for the boolean operators, and with the following rule for UI : ρ, i |= φ1 UI φ2 iff there exists j such that 1. π(i) = (a, τi ) (1) i < j < |ρ|, (2) ρ, j |= φ2 , (3) τj − τi ∈ I, and (4) ρ, k |= φ1 for all k with i < k < j. 2. w[p, hi] = σ0 [p] for every p ∈ P Theorem 2. Let φ be a sentence of MTL. Then |=t-ESG 3. w[p, h(a, τ1 ) , (a, τ2 ) , . . . , (a, τi )i] = σi [p] for every φ iff |=MTL φ. i ∈ N and every p ∈ P 1 Some variants of MTL require (τ ) to be strictly increasing, i which can be represented in t-ESG by requiring strictly increasing Analogously to above, we show that w, zi , π |=t-ESG φ traces. iff ρ, i |= φ by induction over φ. 42 6 Basic Action Theories The precondition axiom states that the robot can (2) start goto if it is currently not performing any Similarly to ES and ESG, a t-ESG BAT is a set of sen- action, (3) stop goto (and reach its destination) if it tences describing the initial situation and the agent’s was moving at least d(s, g) time units, (4) start pick- actions with their preconditions and effects. ing an object if it as the same location as the object, Definition 19 (Basic Action Theory). Given a set of (5) end picking an object if it started picking at least 3 fluent predicates F, a set Σ ⊆ t-ESG of sentences is time units ago, (6) start putting an object to a loca- called a basic action theory over F iff Σ = Σ0 ∪ Σpre ∪ tion if it is holding the object and it is at the location, Σpost , where Σ mentions only fluents in F and (7) end putting an object if it started putting at least 2 1. Σ0 is any set of fluent sentences, time units ago. Additionally, ending any action is only possible if the robot is currently performing the action. 2. Σpre is a set of fluent formulas with free variable The robot’s actions have effects on the following a, predicates: 3. Σpost is a set of sentences, with one sentence of [a]RobotAt(l) ≡ (8) the form [a]f (~x) ≡ γf for each fluent predicate f ∈ F, and one sentence of the form [a]f (~x) = ∃s. a = end goto(s, l))∨ v ≡ γf for each f ∈ H ∪ I, and where γf is a RobotAt(l) ∧ ¬∃s0 , g 0 . a = start goto(s0 , g 0 ) fluent formula. [a]At(o, l) ≡ (9) In a BAT, Σ0 describes the initial situation, Σpost a = end put(o, l) ∨ At(o, l) ∧ a 6= start pick (o) is a set of successor state axioms, and Σpre is a set of [a]Holding(o) ≡ (10) precondition axiom for all actions in the domain that is a = end pick (o)∨ understood disjunctively, i.e., from Σpre , we construct a single precondition axiom of the form Poss(a) ≡ Holding(o) ∧ a 6= start pick (o) [a]Performing(a0 ) ≡ W Σpre . This is slightly different to ES and ESG and (11) allows us to combine multiple basic action theories. a=a ∧ 0 6.1 A Simple Carrier Robot ∃s, g [a = start goto(s, g)] ∨ ∃o [a = start pick (o)] ∨ We present a BAT of a simple robot that can move around and pick up and put down objects. All actions ∃o [a = start put(o)] ∨ Performing(a0 )∧  are modeled as durative actions with start and stop actions. ¬∃s, g [a = end goto(s, g)] ∧ ¬∃o [a = end pick (o)] ∧ Σpre = { ¬∃o [a = end put(o)] ∃s, g. a = start goto(s, g) (2) ∧ ¬∃a0 . Performing(a0 ), The successor state axioms state that (8) the robot is at location l if it stops doing a goto with l as goal ∃s, g. a = end goto(s, g)∧ (3) location, or if it was at that location and did not start Performing(goto(s, g))∧ moving anywhere else, (9) an object o is at location now ≥ time(goto(s, g)) + d (s, g), l if the robot ends putting o to l or if the object was ∃o, l. a = start pick (o)∧ (4) there before and is not being picked up, (10) the robot is holding object o if ends picking up o or if it was RobotAt(l) ∧ At(o, l), holding the object before and does not start putting it ∃o. a = end pick (o)∧ (5) down, (11) the robot is performing action a0 if it starts Performing(pick(o))∧ a0 or it has been performing a0 and does not end a0 . now ≥ time(pick (o)) + 3, As usual in Golog, we define while and if then else as macros: ∃o, l. a = start put(o, l)∧ (6) def Holding(o) ∧ RobotAt(l), while φ do δ done = (φ?; δ)∗ ; ¬φ? ∃o, l. a = end put(o, l)∧ (7) def if φ then δ1 else δ2 fi = [φ?; δ1 ] | [¬φ?; δ2 ] Performing(put(o, l))∧ def now ≥ time(put(o, l)) + 2 if φ then δ1 fi = if φ then δ1 else nil fi } The BAT already allows us to define simple Golog 43 if ¬RobotAt(table) then a simplified version may look as follows: πs. start goto(s, table); end goto(s, table) fi ΣM pre = { while ∃oAt(o, table) do a = start calibration∧ (12) πo. At(o, table)?; state(arm) 6= calibrating∧ start pick (o); end pick (o); start goto(table, shelf ); end goto(table, shelf ); state(arm) 6= calibrated , start put(o, shelf ); end put(o, shelf ); a = end calibration∧ (13) start goto(shelf , table); end goto(shelf , table); time(start calibration) ≥ 5 ∧ done state(arm) = calibrating, Listing 1: An abstract program to clear all objects a = start perception∧ (14) from the table. state(perception) 6= running a = stop perception∧ (15) programs. The program shown in Listing 1 picks up all state(perception) = running} objects from the table and puts them onto the shelf. Given the following initial situation: [a]state(arm) = s ≡ (16) Σ0 = {RobotAt(shelf ), a = start calib ∧ s = calibrating ∨ At(obj1 , table), a = end calib ∧ s = calibrated ∨ At(obj3 , shelf ), s = state(arm) ∧ d(shelf , table) = 20, d(table, shelf ) = 20, a 6= start calib ∧ a 6= end calib ∀o. (o 6= obj1 ∧ o 6= obj3 ) ⊃ ¬∃l. At(o, l)} [a]state(perception) = s ≡ (17) a = start perception ∧ s = running ∨ We can infer that: a = stop perception ∧ s = paused ∨ s = state(perception) ∧ Σ |= [δ]¬∃o. At(o, table) a 6= start perception ∧ a 6= stop perception Σ |= [δ]RobotAt(table) Following the program transition semantics, one ΣM 0 = {state(arm) = uncalibrated possible successful trace of δ is: state(perception) = paused } Using the maintenance BAT, we can formulate a set z = h (start goto(table), 0) , (end goto(table), 20) , of additional constraints that must be satisfied during (start pick (obj1 ), 20) , (end pick (obj1), 23) , the execution of any program δ: (start goto(shelf ), 23) , (end goto(shelf ), 43) ,  JδKG ∃o. Performing(pick (o)) (18) (start put(obj1 ), 43) , (end put(obj1), 45)i  ⊃ state(arm) = calibrated  JδKG ∃o, l. Performing(put(o, l)) (19)  7 Timed Temporal Constraints ⊃ state(arm) = calibrated  JδKG ∃o. Performing(pick (o)) (20) Listing 1 already shows an abstract program that clears ⊃ H≤1 state(perception) = running  the table. However, to execute the program on a real  robot, additional constraints must be satisfied, e.g., JδKG ¬F≤1 ∃o, l.(Performing(pick (o)) (21) the robot’s perception module needs to be enabled ∨ Performing(put(o, l))) before an object is picked up or put down. Instead  ⊃ state(perception) = paused ) of encoding this in the abstract BAT, we provide an additional maintenance BAT which takes care of these The constraints state that (18) if the robot is per- kinds of constraints. Such a maintenance BAT may be forming a pick action, then the arm must be calibrated, generated from platform models as shown in Figure 1, (19) if the robot is performing a put action, then the 44 arm must be calibrated, (20) if the robot is perform- start ing a pick action, then the perception must have been running for at least 1 second, (21) if the robot is not start goto(table) performing a pick or put action in the next second, start calibrate [20, ∞] then the perception should be paused. [5, ∞] end goto(table) start end calibrate start pick(o1) start perception start goto(table) [1, ∞] [20, ∞] [3, ∞] end pick(o1) stop perception end goto(table) [0, 0] start pick(o1) start goto(shelf) [3, ∞] [20, ∞] end pick(o1) end goto(shelf) Figure 3: The STN after all constraints have been start goto(shelf) checked and respective maintenance actions have been [20, ∞] added. end goto(shelf) example, in the node start pick (o1), Constraint 18 is not satisfied. From the platform models, we can Figure 2: The initial STN. generate an action sequence that satisfies the con- straint. In our example, by searching the state au- 7.1 The Constraint Language tomaton in Figure 1, we can generate the sequence As constraint language, we allow a subset of t-ESG. hstart calibrate, end calibratei, which is then added to the STN. Similarly, the perception needs to be running Definition 20 (Constraint). Given a BAT Σ and a before doing a pick. Thus, the action start perception maintenance BAT ΣM . Let φ be a fluent trace formula is added to the STN. By Constraint 20, the perception only mentioning terms from Σ. Let ψ be a fluent trace must have been running for at least 1 second. Thus, formula only mentioning terms from ΣM . Then the the edge from start perception to start pick (o1) has formula θ = φ ⊃ ψ is a constraint formula. the time constraint [1, ∞]. The resulting STN after checking all STN nodes and all constraints is shown in Intuitively, we interpret a constraint φ ⊃ ψ as fol- Figure 3. lows: 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 satisfied. In other words, 8 Conclusion we cannot satisfy a constraint by making φ false. We presented t-ESG, a logic for reasoning about ac- Definition 21 (Constraint Satisfaction). Given a pro- tions that allows the specification of metric temporal gram δ and a BAT Σ, we say that a constraint θ is constraints. t-ESG extends ESG with metric time and satisfied by δ iff temporal operators referring to the past. We showed Σ |= JδKG θ that Metric Temporal Logic (MTL) can be embedded into t-ESG, while ESG cannot be fully embedded into 7.2 Solving Timed Temporal Constraints t-ESG.We presented a constraint language for specify- Using the example above, we now sketch a procedure ing metric temporal constraints on a platform model, that modifies a given action sequence of an abstract and we sketched a translation of those constraints into program to also satisfy the platform constraints. First, Simple Temporal Networks (STNs). Using the solu- we convert the action sequence into a STN, where each tion of the STN, the abstract Golog program can be action of the sequence is a node in the STN. Such a transformed into an action sequence that is executable STN for the program in Listing 1 is shown in Figure 2. on the robot platform, thereby allowing the separation For each node starting at the start node, we now of the abstract agent behavior specification and the check whether each constraint is satisfied. As an details of the platform, even if they are inter-dependent. 45 Acknowledgements [11] Peter Jonsson and Christer Bäckström. A Unify- ing Approach to Temporal Constraint Reasoning. T. Hofmann was supported by the German National Artificial Intelligence, 102(1):143–155, 1998. Science Foundation (DFG) under grant number GL- 747/23-1. [12] Ron Koymans. Specifying Real-Time Properties with Metric Temporal Logic. Real-Time Systems, References 2(4):255–299, 1990. [1] James F Allen. Maintaining Knowledge About [13] Gerhard Lakemeyer and Hector J Levesque. Situ- Temporal Intervals. Communications of the ACM, ations, Si! Situation Terms, No! In Proceedings of 26(11):832–843, 1983. the 9th International Conference on Principles of [2] R. Alur and T.A. Henzinger. Real-Time Logics: Knowledge Representation and Reasoning (KR), Complexity and Expressiveness. Information and pages 516–526, 2004. Computation, 104(1):35–77, 1993. [14] Hector J. Levesque, Raymond Reiter, Yves Les- [3] Rajeev Alur, Tomás Feder, and Thomas A. Hen- perance, Fangzhen Lin, and Richard B. Scherl. zinger. The Benefits of Relaxing Punctuality. Jour- GOLOG: A Logic Programming Language for Dy- nal of the ACM, 43(1), 1996. namic Domains. Journal of Logic Programming, 31(1-3), 1997. [4] Rajeev Alur and Thomas A. Henzinger. Back to the Future: Towards a Theory of Timed Regular [15] John McCarthy. Situations, Actions, and Causal Languages. In Proceedings of the 33rd Annual Laws. Technical report, Stanford University, 1963. Symposium on Foundations of Computer Science, [16] J. Ouaknine and J. Worrell. On the Decidability pages 177–186, 1992. of Metric Temporal Logic. 20th Annual IEEE [5] Jens Claßen. Planning and Verification in the Symposium on Logic in Computer Science (LICS’ Agent Language Golog. PhD thesis, RWTH Aachen 05), pages 188–197, 2005. University, 2013. [17] Joël Ouaknine and James Worrell. Some Recent [6] Jens Claßen and Gerhard Lakemeyer. A Logic for Results in Metric Temporal Logic. Lecture Notes Non-Terminating Golog Programs. In Proceedings in Computer Science, 5215 LNCS:1–13, 2008. of the 11th International Conference on Principles [18] Javier Pinto and Raymond Reiter. Reasoning of Knowledge Representation and Reasoning (KR), About Time in the Situation Calculus. Annals pages 589–599, 2008. of Mathematics and Artificial Intelligence, 14(2- 4):251–268, 1995. [7] Giuseppe De Giacomo, Yves Lespérance, Hector J Levesque, and Sebastian Sardina. IndiGolog: A [19] Raymond Reiter. Natural Actions, Concurrency High-Level Programming Language for Embedded and Continuous Time in the Situation Calculus. Reasoning Agents. In Multi-Agent Programming. In Proceedings of the 5th International Conference Springer, 2009. on Principles of Knowledge Representation and Reasoning (KR), pages 2–13, 1996. [8] Rina Dechter, Itay Meiri, and Judea Pearl. Tem- poral Constraint Networks. Artificial Intelligence, [20] Raymond Reiter. Knowledge in Action: Logical 49(1-3):61–95, 1991. Foundations for Specifying and Implementing Dy- namical Systems. MIT Press, 2001. [9] Alberto Finzi and Fiora Pirri. Representing Flexi- ble Temporal Behaviors in the Situation Calculus. [21] Stefan Schiffer, Andreas Wortmann, and Gerhard In Proceedings of the 19th International Joint Con- Lakemeyer. Self-Maintenance for Autonomous ference on Artificial Intelligence (IJCAI), pages Robots controlled by ReadyLog. In Proceedings of 436–441, 2005. the 7th IARP Workshop on Technical Challenges for Dependable Robots, 2010. [10] Till Hofmann, Victor Mataré, Stefan Schif- fer, Alexander Ferrein, and Gerhard Lakemeyer. Constraint-Based Online Transformation of Ab- stract Plans into Executable Robot Actions. In AAAI Spring Symposium: Integrating Representa- tion, Reasoning, Learning, and Execution for Goal Directed Autonomy, 2018. 46