In this paper, we propose a formulation of temporal planning in which plans are to be interpreted as a high-level specification of the desired behavior of a control system [cassandras:des, lee:embedded_systems], in which one can discern several discrete devices or agents that need to act in a coordinated way. Figure LABEL:fig:planning_control_systems locates planning algorithms (planners) in the context of Control Systems as the component that provides a reference signal $r(t)$ that informs a suitably designed controller component. Planning and control take place at two different time-scales. Planners are bound to a planning cycle of variable duration that is as long as the controller takes to implement a plan, or until whatever point in time a supervisory system, not shown in Figure LABEL:fig:planning_control_systems and either automated or directly operated by a human, interrupts execution. Controllers are bound to a control cycle, whose duration is fixed and its value chosen as part of the design. Controllers compute control signals $u(t)$, which are meant to drive the behavior, or output signal $y(t)$, of the plant. Generally, $y(t)$ is not directly observable, so a state estimation component is needed that integrates information collected about changes in $y(t)$ over time to produce a state signal $x(t)$. The control function $g(\cdot,\cdot)$ is subject to several constraints. To wit, it can only utilize the information obtained by the state estimation procedure; it must minimize some measure of tracking error between the required behavior $r(t)$ and the (indirectly observed) actual behavior $y(t)$, and it must do so within a given time limit that defines the duration of a control cycles. Solutions to $g(\cdot,\cdot)$ are thus expected to compensate for any disturbance. Disturbances are a general concept in Control Theory covering a vast collection of phenomena ranging from non-determinism in the plant, e.g. delays of changes in $y(t)$ due to changes in $u(t)$, to misalignment between reality and the abstractions of and assumptions on crucial characteristics of the dynamics of non-planning components in Fig. LABEL:fig:planning_control_systems, that the planner uses to design $r(t)$. The analytical framework to study and verify formal properties of systems like those in Fig. LABEL:fig:planning_control_systems is that of Hybrid System Theory [tabuada:hybrid], but in this work we do not concern ourselves with the research questions that arise from supervisory components interrupting the current plan and switching to another one, and thus omit further discussion of the hybrid nature of these systems.

0.1 Domain Theories from System Models

[width=]img/system_with_planner.drawio.pdf

Figure 1: Refinement of Figure LABEL:fig:semi_autonomous_system_architecture in which we identify two new sub-systems in the executive control (supervisor and control) and physical system models (plant and measurement). The diagram also makes explicit the possibility of plans defining the control for multiple types of autonomous systems that need to act in a co-ordinated manner. See text for details and discussion.

We address now the provenance of the domain theories of interest to our research, that aim at representing in operationally meaningful ways the structure of states and inputs to dynamical systems with a structure like the one shown in Figure LABEL:fig:planning_control_systems. Equipped with these, it then becomes possible to encode facts and assumptions about dynamical systems in a symbolic manner, enabling general but suitably engineered algorithms to reason about the existence of arbitrarily complex properties, such as the existence of plans. We follow loosely the presentation in [lee:embedded_systems, cassandras:des].

A model of a dynamical system is given by a differential or integral equation that relates so-called input signals, for instance force and torque for a mechanical system, to output signals, like position, orientation or rotational velocity. Any such system can in turn be considered a component into a larger one. A model of a system is thus given by a function of the form $S:{\cal X}\to{\cal Y}$, where ${\cal X}={\cal Y}=\mathbb{R}^{\mathbb{R}}$, that is the set of functions that map the reals into the reals. The domain of functions in sets ${\cal X}$ and ${\cal Y}$ have time as their domain, and their codomain represents the value of the signal at a given time. In Figure LABEL:fig:planning_control_systems we illustrate a typical decomposition of $S$ into three smaller sub-systems: a controller component, a state estimation component, and finally, the so-called plant, a physical model of the object to be controlled and its environment. We now discuss each of these, and formalize the fine-grained structures in systems $S$ depicted in Figure LABEL:fig:planning_control_systems.

0.1.1 System State Models

A more useful system model follows from identifying a set of functions from $\mathbb{T}$ to $\thereals^{n}$, where $n$ can vary from function to function, and the mathematical relationships between their values in different time instants. These functions, or signals, respond to specific assumptions. So-called output variables, denoted by a vector functions $\mathbf{y}(t)=[y_{1}(t)\,\ldots\,y_{m}(t)]^{T}$, are those signals that can be measured directly. The signals that are assumed to be controllable receive the name of input variables and are denoted by $\mathbf{u}(t)=[u_{1}(t)\,\ldots\,u_{p}(t)]^{T}$. Finally, signals that convey the information necessary to predict values of $\mathbf{y}(t)$ given a measurement $\mathbf{y}(t_{0})$, $t_{0}<t$, and inputs $\mathbf{u}(t^{\prime})$ for $t^{\prime}\in[t_{0},t)$ are referred to as state variables and denoted by $\mathbf{x}(t)=[x_{1}(t)\ldots x_{d}(t)]^{T}$. State variables in a system model can include output variables when these are observable and otherwise follow from a non-trivial estimation process as depicted in Figure LABEL:fig:planning_control_systems.

As advanced in the Introduction, we consider discrete-time system models, models in which  is set to . We note that proceeding in this way does not require to discretize signal values. The set of possible values of signals are, respectively, $U\subset\thereals^{p}$, $Y\subset\thereals^{m}$, and $X\subset\thereals^{d}$, for control, output and state signals. Then, functions $\mathbf{u}(t)$, $\mathbf{y}(t)$ and $\mathbf{x}(t)$ become sequences $\mathbf{u}(k)$, $\mathbf{y}(k)$ and $\mathbf{x}(k)$, where $k=\lfloor t/T_{s}\rfloor$, and $T_{s}>0$ is a fixed sample period. A state-based model thus consists of the above definitions and equations

$$\mathbf{x}(k+1) =\mathbf{f}(\mathbf{x}(k),\mathbf{u}(k),k),\;\mathbf{x}(0)=\mathbf{x}_{0}$$ (1a)

$$\mathbf{y}(k) =\mathbf{h}(\mathbf{x}(k),\mathbf{u}(k),k)$$ (1b)

with $\mathbf{f}$, $\mathbf{h}$ being difference rather than differential equations, and $\mathbf{x}_{0}$ being a given initial condition for the system.

0.1.2 Strictly Causal Systems

Equations (1a) and (1b) capture a very general class of systems (Figure LABEL:fig:planning_control_systems). In this paper, we assume that the system of interest is time-invariant and strictly causal [lee:embedded_systems], both properties crucial for the design of feedback control systems. A system is causal if its output $\mathbf{y}(k)$ only depends on current and past inputs. Formalizing this dependency requires to introduce new notation and definitions. Let us consider a continuous-time signal $s:\mathbb{R}\to A$, for some set $A$. Let $s\mid_{t\leq\tau}$ be a partial function, or restriction in time, that is only defined for $t\leq\tau$, and when it is so we have that $s\mid_{t\leq\tau}(t)=s(t)$. As a result, if $s$ is an input to a system, then $s\mid_{t\leq\tau}$ is the “current and past inputs” at time $t$.

Now let us consider a continuous-time system $S:{\cal X}\to{\cal Y}$, where ${\cal X}=A^{\mathbb}{R}$ and ${\cal Y}$ $=$ $B^{\mathbb}{R}$, the sets of functions, respectively, from $\mathbb{R}$ to some set $A$ (resp. some set $B$). We say that $S$ is causal if for all functions $x_{1},x_{2}\in{\cal X}$ and $\tau\in\mathbb{R}$

$$x_{1}\mid_{t\leq\tau}=x_{2}\mid_{t\leq\tau}\rightarrow S(x_{1})\mid_{t\leq\tau}=S(x_{2})\mid_{t\leq\tau}$$

In words, the system $S$ is causal if for two possible inputs $x_{1}$ and $x_{2}$ that are identical up to and including time $\tau$, the outputs of $S$ are also identical up to and including time $\tau$. A system $S$ is strictly causal if for all $x_{1}$, $x_{2}$ $\in$ $X$ and $\tau\in\mathbb{R}$

$$x_{1}\mid_{t<\tau}=x_{2}\mid_{t<\tau}\rightarrow S(x_{1})\mid_{t\leq\tau}=S(x_{2})\mid_{t\leq\tau}$$

That is, $S$ is strictly causal if for possible inputs $x_{1}$ and $x_{2}$ identical, but crucially, not including time $\tau$. In contrast, the outputs are identical up to and including $\tau$. The output of $S$ at time $t$ of a strictly causal system does not depend on its inputs at time $t$. It does so only on past inputs. This property is crucial when it comes to the design of $g(x,r)$ in Figure LABEL:fig:planning_control_systems, as no control function $g$ can exist that changes its output without a change in its inputs at least one control cycle before, if the system $S$ is to be strictly causal. The assumptions of time-invariance and strict causality simplify (1a) and (1b)

$$\mathbf{x}(k+1) =\mathbf{f}(\mathbf{x}(k),\mathbf{u}(k)),\;\mathbf{x}(0)=\mathbf{x}_{0}$$ (2a)

$$\mathbf{y}(k) =\mathbf{h}(\mathbf{x}(k))$$ (2b)

We note that strict causality makes irrelevant some of the temporal predicates in Table LABEL:tab:IL_predicates, like $\Starts{X}{Y}$, to model interactions between system inputs and outputs. As established by the definitions of causality and strict causality for systems $S$, a controller cannot decide at control cycle $k$ to initiate actions or stop ongoing ones based on a change between $y(k-1)$ and $y(k)$, or between $r(k-1)$ and $r(k)$. It is only possible to do so for if changes are observed before or exactly at $k-1$. As a result, we do not use the temporal relations that violate these properties to establish relations between TQAs that represent properties of state and input signals.

0.1.3 Logic Theories of Systems

The domain theories $(\Sigma,V)$ we consider in this paper include state-based models. Therefore, $\Sigma$ contains standard definitions of functions and predicates in the theory of arithmetic over the reals, and $V$ includes a possibly infinite set of real-valued logical variables. $\Sigma$ also contains predicates defined from combining standard ones such as “$\leq$” via the logical connectives $\land$ or $\lor$. Furthermore, the left and right-hand sides of Eqs. (1a)–(1b) are terms in ΣV, and since “$=$” has a standard definition too, the equations are elements of ΣV, and provide a system-specific set of invariant properties or axioms.

In contrast, transient properties are described by formulas in ΣV which only hold for specific periods of time and denote subsets of (or combinations thereof) $U$, $X$, and $Y$. The histories $h$ used to define the satisfiability of IL formulas $\varphi$ are obtained directly from sequences $\mathbf{x}(k)$, $\mathbf{u}(k)$ and $\mathbf{y}(k)$

$$h(k,\varphi)=\begin{cases}1&\mathrm{if}\,\mathbf{x}(k),\mathbf{u}(k),\mathbf{y}(k)\models\varphi\\ 0&\mathrm{otherwise}\end{cases}$$ (3)

so that the truth of $\varphi$ is interpreted according to the definitions of the symbols therein, and the values taken by state, input and output signals. We next present an illustrative example of a logical theory representing maneuvers for a widely studied class of vehicles known as differential drive systems [klancar:wheeled].

0.2 Maneuvers for a Differential Drive System

TODO: The construction of logical theories is driven by a concrete purpose, in our case, we want to capture

[width=]img/turn_maneuver.drawio.pdf

Figure 2: Turning maneuver modeled with Interval Logic. White rectangles are intervals, and text near the left end-point is the name used in the example below ($I_{A}$), centered text indicates the formula attached to them e.g. $Near(l_{0})$.

Differential drive is a simple driving mechanism with wide practical applications for small robots [klancar:wheeled]. A discrete-time state-model for such robots is

$$x(k+1) =x(k)+v(k)T_{s}\cos(\phi(k))$$

$$y(k+1) =y(k)+v(k)T_{s}\sin(\phi(k))$$

$$\phi(k+1) =\phi(k)+\omega(k)T_{s}$$

obtained from the continuous-time model via Euler integration, where $T_{s}$ is the sampling interval. In this model, output variables, $x(k),y(k),\phi(k)$ describe the position and the bearing of the robot, while $v(k)$ and $\omega(k)$ are the inputs. Furthermore, all output variables are also state variables. Many domain theories $(\Sigma,V)$ are possible for this model, their differences stemming from the purpose of the system. For a robot meant to transport cargo in a warehouse, a useful predicate is

$$Near(l)\equiv\sqrt{(x-x_{l})^{2}+(y-y_{l})^{2}}\leq d_{l}$$ (4)

where $x,y\in V$, $l$ is a natural number indexing locations, and $x_{l},y_{l},d_{l}$ are constants in $\Sigma$. Another useful predicate is

$$Pointing(l)\equiv|\phi-\arctan(x_{l}-x/y_{l}-y)|<e_{l}$$ (5)

which is true whenever the robot bearing points toward location $l$. To change the outputs of the system, and hence the truth of formulas using these two predicates, an input signal must be applied to the system. For instance, setting the inputs to follow a control law to turn the robot towards a location $l$ is represented by the predicate

$$Turn(l)\equiv\omega(k+1)=\omega(k)+K_{1}e(k)-K_{2}T_{s}\omega(k)T_{s}$$ (6)

where $e(k)=\arctan(x_{l}-x(k)/y_{l}-y(k))-\phi(k)$, and $K_{1}$, $K_{2}$ are positive constants. The (multi-dimensional) reference signal $r(t)$ is then captured exactly by the following following conjunction of TQAs and temporal constraints

$$Turn(l_{1})_{I_{D}} \land Near(l_{0})_{I_{A}}\land Align(l_{0})_{I_{B}}\land Align(l_{1})_{I_{C}}$$

$$\land I_{A}\supset I_{D}\land I_{B}\frown I_{D}\land I_{D}\frown I_{C}$$

and is depicted in Figure 2, and is useful to interpret the above as a time diagram like those typically used in digital logic, where we have one binary signal for each predicate. Temporal constraints indicate how the periods during which signals are true or false overlap or follow each other. Changes in the truth values of $Pointing(l_{0})$ and $Pointing(l_{1})$ are not exactly synchronized with the end-points of $I_{turn}$, as the $Pointing$ predicate allows some deviation, bounded by the constant $e_{l}$.