Linear logic as a tool for planning under temporal uncertainty (Q534715): Difference between revisions
From MaRDI portal
Created a new Item |
Changed an Item |
||
Property / review text | |||
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. | |||
Property / review text: 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. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Eric Martin / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68T27 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 03F52 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 5886389 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
linear logic | |||
Property / zbMATH Keywords: linear logic / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
planning under uncertainty | |||
Property / zbMATH Keywords: planning under uncertainty / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
winning strategies | |||
Property / zbMATH Keywords: winning strategies / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
proofs-as-programs paradigm | |||
Property / zbMATH Keywords: proofs-as-programs paradigm / rank | |||
Normal rank |
Revision as of 09:44, 1 July 2023
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Linear logic as a tool for planning under temporal uncertainty |
scientific article |
Statements
Linear logic as a tool for planning under temporal uncertainty (English)
0 references
10 May 2011
0 references
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.
0 references
linear logic
0 references
planning under uncertainty
0 references
winning strategies
0 references
proofs-as-programs paradigm
0 references