2-APL UPC project.
second part of formal semantics done :)
+64
-2
+64
-2
docs/2apl-doc.tex
+64
-2
docs/2apl-doc.tex
···
514
514
515
515
Let $A_{\iota}$ be the configuration of agent $\iota$ and let $\chi$ be a set of external shared environments each of which is a consistent set of atoms. the configuration of a 2APL multi-agents system is defined as $ \langle A_{1}, \ldots, A_{n}, \chi \rangle $.
516
516
517
+
\subsubsection{Transition rules for basic actions}
518
+
519
+
A basic action can be executed at individual agent level. For some types of basic actions additional transition rules are given that specify when an action's execution fails and which transition an individual agent should make if the execution of the action fails. In general when the execution of a basic action fails, an exception with its corresponding plan identifier, is added to the set of failed plans. This exception can later be used to repais the corresponding plan by meabs of plan repair rules.
517
520
518
-
\subsubsection{Transition rules for basic actions}
521
+
Now, we present the differents transition rules that capture the execution of basic actions. We assume $\gamma \vDash_{g} \texttt{true}$ for any goal base $\gamma$. We use $G(r)$, $B(r)$ and $P(r)$ to indicate the head $\kappa$, the belief condition $\beta$, and the plan $\pi$ of a rule $r = (\kappa \leftarrow \beta \vert \pi)$.
519
522
520
523
\paragraph{Skip action}
524
+
525
+
The execution of \texttt{skip} action has no effect on an agent's configuration. The execution of
526
+
this action always succeeds resulting in its removal from the plan base.
527
+
521
528
$$ {{\gamma \vDash_{g} G(r)}\over{\langle \iota, \sigma, \gamma, \{(\texttt{skip}, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota, \sigma, \gamma, \{\}, \theta, \xi \rangle}}$$
522
529
530
+
This transition indicates that the execution of the plan entry $(\texttt{skip}, r, id)$ proceeds resulting in the removal os this entry from the plan base. This transition rule can be applied only if the goal that is assigned to the \texttt{skip} action is entailed by the agent's goal base.
531
+
523
532
\paragraph{Belief update action}
533
+
534
+
A belief update action, which is specified in terms of a pre- and a post-condition, modifies the belief base when it is executed. A belief update action can be executed if its pre-condition is entailed by the belief base. After the execution of the action, its post-condition should be entailed by the belief base. The modification of the belief base to entail the post-condition is realized by adding positive literals of the post-condition to the belief base and removing the atoms of negative literals of the post-condition from the belief base.
535
+
536
+
A successful execution of a belief update action $\alpha$ is then defined as follows.
537
+
524
538
$$ {{T(\alpha \theta, \sigma) = \sigma' \& \gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(\alpha, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota, \sigma', \gamma', \{\}, \theta, \xi \rangle}} $$
525
-
539
+
540
+
where $T$ is a function that takes a belief update action and a belief base, and returns the modified belief base if the pre-condition of the action is entailed by the agent's belief base.
541
+
542
+
The beliefs and goals of agents are related to each other. In fact, if an agent believes a
543
+
certain fact, then the agent does not pursue that fact as a goal. This means that if an agent
544
+
modifies its belief base, then its goal base may be modified as well.
545
+
526
546
\paragraph{Test action}
547
+
548
+
The objective of a test action is to check if the belief and goal queries within a test expression are entailed by the agent's belief and goal bases. Since we have the substitution $\theta$ that should be applied to the variables in the test expression, this can still contain unbound variables. Therefore, the test action results in another substitution $\tau$ added to $\theta$.
549
+
550
+
A test action $\varphi$ can be exevuted successfully if $\varphi$ is entailed by the agent's belief and goal bases.
551
+
527
552
$$ {{( \sigma, \gamma) \vDash_{t} \varphi \theta \tau \& \gamma \vDash_{g} G(r)}\over{\langle \iota, \sigma, \gamma, \{(\varphi, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota, \sigma, \gamma, \{\}, \theta \cup \tau, \xi \rangle}} $$
528
553
554
+
A test action can fail if one or more of its involved query expressions are not entailed by the belief or goal bases. In such a case, the test action remains in the agent's plan base and an exception is generated to indicate the failure of this action.
529
555
530
556
\paragraph{Goal dynamics actions}
557
+
558
+
Goals can be adopted and added to the agent's goal base by means of basic actions $\texttt{adopta}(\phi)$ and $\texttt{adoptz}(\phi)$ . The first action adds the goal $\phi$ to the beginning of the goal base and the second action adds the goal $\phi$ to the end of the goal base.
559
+
531
560
$$ {{{\sigma \nvDash \phi \theta} \& {\texttt{ground}(\phi \theta)} \& {\gamma \vDash_{g} G(r)}}\over{\langle \iota, \sigma, \gamma, \{(\texttt{adoptX}(\phi), r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota, \sigma, \gamma', \{\}, \theta, \xi \rangle}} $$
532
561
562
+
If the agent believes that the goal to be adopted is already achieved (i.e., if the goal is entailed by the agent's belief base) or if the goal to be adopted is not ground, then the action is considered as failed. The action remains in the agent’s plan base and an exception is generated.
563
+
564
+
Goals can be dropped and removed from the goal base by means of $\texttt{dropgoal}(\phi)$, $\texttt{dropsubgoals}(\phi)$, and $\texttt{dropsupergoals}(\phi)$ actions. The first action removes from the goal base the goal $\phi$, the second removes all goals that are subgoals of $\phi$, and the third action removes all goals that have $\phi$ as a subgoal.
565
+
533
566
$$ {{\gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(\texttt{dropX}(\phi), r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota, \sigma, \gamma', \{\}, \theta, \xi \rangle}} $$
534
567
568
+
The three dropping goal actions will always succeed, even if there is no goal to be removed from the goal base.
535
569
536
570
\paragraph{Abstract action}
571
+
572
+
Abstract actions are representations of plans. The execution of an abstract action replaces the action with the plan it represents. The relation between an abstract action and the plan it represents is specified by means of a procedure call rule (PC-rule) that has a head unificable with the abstract action.
573
+
574
+
Let $\alpha$ be an abstract action, $\varphi \leftarrow \beta \vert \pi$ be a variant of a PC-rule of agent and Unify be a function that returns the most general unifier of $\alpha$ and $\varphi$ if they are unifiable, otherwise it returns $\bot$. A successful execution of an abstract action will replace it with a plan.
575
+
537
576
$$ {{Unify(\alpha\theta, \phi = \tau_{1} \& \sigma \vDash \beta\tau_{1}\tau_{2} \& \gamma \vDash_{g} G(r) } \over {\langle \iota, \sigma, \gamma, \{(\alpha, r, id)\}, \theta, \xi \rangle \rightarrow \langle \iota, \sigma, \gamma', \{(\pi\tau_{1}\tau_{2}, r, id)\}, \theta, \xi \rangle}} $$
538
577
578
+
If there is no PC-rule applicable (i.e., a PC-rule is not applicable if either its head cannot be unified with the abstract action or its belief condition is not entailed by the belief base), then the execution of the abstract action is considered as failed.
579
+
539
580
\paragraph{Communication actions}
540
581
582
+
Agents can communicate with each other by sending messages to each other. An agent can send a message to another agent by means of the send(j, p, l, o, φ) action. The execution of the send action broadcasts a message which will be added to the event base of the receiving agent. The broadcasted message will include the name of the sending agent.
583
+
584
+
${\varphi = \langle \iota, j, p, l, o, \phi \rangle} \& \gamma \vDash_{g} G(r))\over{ \langle \iota, \sigma, \gamma, \{(\texttt{send}(j, p, l, o, \phi),r, id)\}, \theta, \xi \langle \underrightarrow{\varphi\theta!} \langle \iota, \sigma, \gamma, \{\}, \theta, \xi \rangle}$
585
+
586
+
The broadcasting of the message is indicated buy de exclamation mark in $\varphi\theta!$ which means that the transitions proceeds by broadcasting the message event.
587
+
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
+
590
+
541
591
\paragraph{External actions}
592
+
593
+
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.
594
+
595
+
We assume that there is no time between performing an action in an environment and the reception of the return value, so no other external action can be executed between performing an external action and the reception of its corresponding return value.
596
+
597
+
This assumption implies that external actions are blocking actions, but it does not mean that the execution of an agent's plan should wait until the actual and intended effect of the action is realized.
598
+
599
+
The transition for external actions broadcast an event to the multi-agent system level and waits for the return value from the environment in one transition step.
600
+
601
+
$$ {t \neq \bot & \gamma \vDash_{g} G(r)} \over {\langle \iota, \sigma, \gamma, \{(@env(\alpha(t_{1}, \ldots, t_{n}), V), r, id)\},\theta, \xi \rangle \underrightarrow{nv(\alpha(t_{1}\theta, \ldots, t_{n}\theta), t)} \langle \iota, \sigma, \gamma, \{\}, \theta \cup \{ V \diagup t\}, \xi \rangle } $$
602
+
603
+
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.
542
604
543
605
544
606
\subsubsection{Transition rules for plans}