Linear logic as a tool for planning under temporal uncertainty (Q534715)

The paper starts with the illustrative example of the following plan: a ship that needs between 2 to 5 days to reach its destination is serviced on a normal dock for 2 or 3 days if it arrives within 4 days; otherwise a reservation is made on day 4 for the express dock, precisely two days before it will be serviced, in 1 day. In any case, the ship will have been serviced within 7 days. This example illustrates a form of ``temporal uncertainty about the effects of actions, where time duration does matter'', and necessitates ``preemptive/anticipative actions'' to guarantee success. The authors view this kind of planning problem as a game between Controller and Nature: Controller performs a move of the form \(\text{flash}_\beta\) or \(\text{go}_\beta\) for an action \(\beta\) that is instantaneous or might incur delays before it is completed, respectively, provided the ``enabling conditions for \(\beta\)'' hold; Nature performs a move of the form \(\text{end}_\beta\) to decide when noninstantaneous action \(\beta\) is completed within a given time interval. Controller is after a winning strategy, starting from an initial state \(W\), characterised by a tree of all possible trajectories that all end in a member of the set \(Z\) of admissible final states, at in time that belongs to a priorly given interval \([A_0,B_0]\), and such that all actions that have been started have ended. In principle, a node associated with a noninstantaneous starting action will have an outgoing edge labeled with some time \(t\) for all possible values of \(t\) in some time interval, but branches can be glued and, provided that the number of states and the number of actions are both finite, then any winning strategy can be adjusted to a winning strategy represented but a tree of bounded height, as shown in the first theorem of the paper and illustrated with the introductory example. Then the authors show how to use sequents of linear logic as a specification language. For instance, thanks to \(d_\alpha(\infty)\) denoting that action \(\alpha\) is not active for the time being, a sequent of the form \[ (\text{T}(t)\otimes s\otimes d_\alpha(\infty))\vdash(\text{T}(t)\otimes\widetilde{s}\otimes\exists\rho((a\leq\rho\leq b)\otimes d_\alpha(t+\rho))) \] expresses that action \(\alpha\) is fired at time \(t\), with state \(s\) being modified to intermediate state \(\widetilde{s}\), the expecting time delay being in the range \([a,b]\) and recorded by \(d_\alpha\), whereas a sequent of the form \[ (\text{T}(t')\otimes\widetilde{s}\otimes d_\alpha(t'))\vdash(\text{T}(t')\otimes s'\otimes d_\alpha(\infty)) \] expresses that action \(\alpha\) is completed at time \(t'\) recorded by \(d_\alpha\), with \(\widetilde{s}\) being modified into the proper state \(s'\). The complete specification for the introductory example is provided, before the equivalence between a winning stately and an LL proof for this example is demonstrated, which involves, besides the inference rules of intuitionistic affine logic, that is, first-order linear logic enriched with the weakening rule, valid axioms about real time in the form of linear equalities and inequalities such as \[ ((2\leq\rho\leq 3)\otimes(2\leq t_2<4)\otimes(t_7=t_2+\rho))\vdash(0<t_7\leq 7). \] The authors then prove the main result of the paper, a completeness result which shows the equivalence between the existence of a winning strategy and the provability of \[ \Big(\text{T}(0)\otimes W\otimes\bigotimes_\alpha d_\alpha(\infty)\Big)\vdash\exists t'\big((A_0\leq t'\leq B_0)\otimes\text{T}(t')\otimes\overline{Z}^\oplus\times\bigotimes_\alpha d_\alpha(\infty)\Bigl). \] The paper ends with a discussion of the merits of the proposed formalism as opposed to existing alternatives.