Linear logic as a tool for planning under temporal uncertainty (Q534715): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(6 intermediate revisions by 5 users not shown) | |||
Property / author | |||
Property / author: Max I. Kanovich / rank | |||
Property / author | |||
Property / author: Max I. Kanovich / rank | |||
Normal rank | |||
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 / 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 | |||
Property / reviewed by | |||
Property / reviewed by: Eric Martin / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.027 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1983464388 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A theory of timed automata / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Weak, strong, and strong cyclic planning via symbolic model checking / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Managing concurrency in temporal planning using planner-scheduler interaction / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2734937 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q5313998 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4842966 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic as a logic of computations / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The classical AI planning problems in the mirror of Horn linear logic: semantics, expressibility, complexity / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Strong planning under uncertainty in domains with numerous but identical elements (a generic approach) / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2734936 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Generating plans in linear logic. I: Actions as proofs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Generating plans in linear logic. II: A geometry of conjunctive actions / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q2755109 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 01:28, 4 July 2024
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
0 references
0 references