2-APL UPC project.
third part of formal semantics done :)
+31
-5
+31
-5
docs/2apl-doc.tex
+31
-5
docs/2apl-doc.tex
···
587
587
588
588
The send action will always succeed. A 2APL agent is assumed to be able to receive a message that is sent to it at any time. The received message is added to the event base of the agent.
589
589
590
-
591
590
\paragraph{External actions}
592
591
593
592
The execution of an external action by an individual agent affects the external environments that may be shared by other agents. An environment returns in turn a value back to the agent, which can be either some result of the successfully performed action (in the form of a list of terms) or $\bot$ indicating that the execution of the action is failed.
···
602
601
603
602
If the return value is a failure exception, then the execution of the external action is considered as failed. As a consequence, the action is not removed from the plan base and its identifier is added to the agent's event base.
604
603
605
-
606
604
\subsubsection{Transition rules for plans}
607
605
606
+
In this section, we present the transition rules that capture the execution of plans consisting of basic actions composed by sequence, conditional choice, conditional iteration, and non-interleaving operators.
607
+
608
608
\paragraph{Sequence plan}
609
+
610
+
The execution of a sequence plan $\alpha; \pi$ consists of the execution of the basic action $\alpha$ followed by the execution of plan $\pi$. Thus, an agent with a sequence plan $\alpha; \pi$ can make a transition through which the first basic action $\alpha$ is executed. The rest $\pi$ of the plan remains in the resulting configuration.
611
+
609
612
$${ {\langle \iota, \sigma, \gamma, \{(\alpha, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota', \sigma', \gamma, \{\}, \theta', \xi' \rangle} \over {\langle \iota, \sigma, \gamma, \{(\alpha:\pi, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota', \sigma', \gamma, \{(\pi, r, id)\}, \theta', \xi' \rangle}}$$
610
613
611
614
\paragraph{Conditional plan}
615
+
616
+
The execution of a conditional plan {\tt if $\varphi$ then $\pi_{1}$ else $\pi_{2}$} consists of a choice between plans $\pi_{1}$ and $\pi_{2}$. The condition $\varphi$ is evaluated with respect to the agent's belief and goals base. If the the agent's belief and goal base entails the condition, then $\pi_{1}$ will be selected, otherwise plan $\pi_{2}$ is selected. If the conditional plan has no 'else' part, this will be considered as a \texttt{skip} plan.
617
+
612
618
$${ {(\sigma, \gamma) \vDash_{t} \varphi\theta\tau \& \gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(\texttt{if} \varphi \texttt{then} \pi_{1} \texttt{else} \pi_{2}, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota, \sigma, \gamma, \{(\pi_{1}\tau, r, id)\}, \theta, \xi \rangle}}$$
613
619
\vskip 0.2ex
614
-
$${ {�\exists\tau : (\sigma, \gamma) \vDash_{t} \varphi\theta\tau \& \gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(\texttt{if} \varphi \texttt{then} \pi_{1} \texttt{else} \pi_{2}, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota', \sigma', \gamma, \{(\pi_{2}\tau, r, id)\}, \theta, \xi \rangle}}$$
615
-
620
+
$${ {¬\exists\tau : (\sigma, \gamma) \vDash_{t} \varphi\theta\tau \& \gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(\texttt{if} \varphi \texttt{then} \pi_{1} \texttt{else} \pi_{2}, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota', \sigma', \gamma, \{(\pi_{2}\tau, r, id)\}, \theta, \xi \rangle}}$$
621
+
622
+
The execution of conditional plans will always succeed.
623
+
624
+
616
625
\paragraph{While plan}
626
+
627
+
The execution of a while plan {\tt while $\varphi$ do $\pi$} depends on if $\varphi$ is entailed by the agent's belief and goal bases, then the plan $\pi$ should be executed after which the while plan should be tried again.
628
+
617
629
$${ {(\sigma, \gamma) \vDash_{t} \varphi\theta\tau \& \gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(\texttt{while} \varphi \texttt{do} \pi, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota', \sigma', \gamma, \{(\pi\tau;\texttt{while} \varphi \texttt{do} \pi, r, id)\}, \theta, \xi \rangle}}$$
618
630
\vskip 0.2ex
619
631
$${ {¬\exists\tau:(\sigma, \gamma) \vDash_{t} \varphi\theta\tau \& \gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(\texttt{while} \varphi \texttt{do} \pi, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota', \sigma', \gamma, \{\}, \theta, \xi \rangle}}$$
620
-
632
+
633
+
The execution of a while loop always succeed.
634
+
621
635
\paragraph{Atomic plan}
622
636
637
+
The execution of an atomic plan is the non-interleaved execution of the maximum number of actions of the plan. An atomic plan can be defined like $[\alpha_{1} ; \ldots ; \alpha_{n} ]$, where $\alpha_{i}$ is an action. The following transition rule specifies the execution of atomic plan.
638
+
639
+
$$ {(\forall_{i} : 1 \leq i \leq m \rightarrow transition(A_{i}, A{i+1})) & \forall A: ¬transition(A_{m+1}, A)} \over { \langle \iota, \sigma_{1}, \gamma_{1}, \{([\alpha_{1} ; \ldots ; \alpha_{n} ],r, id)\}, \theta_{1}, \xi_{1} \rangle \rightarrow \langle \iota, \sigma_{m+1}, \gamma_{m+1}, \Pi, \theta_{m+1}, \xi_{m+1}\rangle}$$
640
+
641
+
This transition rule defines the transition of one initial configuration of an agent, to a final configuration, executing each intermediate transition.
642
+
623
643
\paragraph{Multiple concurrent plans}
644
+
645
+
An agent executes its plans concurrently by interleaving the executions of their constituent actions. An agent executes one of its plans at each computation step, as we can see in the following transition.
646
+
647
+
$$ {\langle \iota, \sigma, \gamma, \rho, \theta, \xi \rangle \rightarrow \langle \iota, \sigma', \gamma', \rho', \theta', \xi' \rangle } \over {\langle \iota, \sigma, \gamma, \Pi, \theta, \xi \rangle \rightarrow \langle \iota, \sigma', \gamma', \Pi', \theta', \xi' \rangle}$$
648
+
649
+
where $\rho = \{\pi, r, id} \subset \Pi $ and $\Pi' = (\Pi \diagdown \rho) \cup \rho'$.
624
650
625
651
\subsubsection{Practical reasoning rules}
626
652