2-APL UPC project.
first point of formal semantics done
+36
-19
+36
-19
docs/2apl-doc.tex
+36
-19
docs/2apl-doc.tex
···
491
491
492
492
In this section we present the formal semantics of 2APL in terms of transition system. A transition system is a set of transition rules for deriving transitions. A transitionis is a transformation of one configuration into another and it corresponds to a simple computation/execution step.
493
493
494
-
%% TODO
494
+
The execution of a 2APL multi-agent program modifies its initial configuration by means of transitions that are derivable from the transition rules. In fact, each transition rule indicates which execution step (i.e., transition) is possible from a given configuration. It should be noted that for a given configuration there may be
495
+
several transition rules applicable. An interpreter is a deterministic choice of applying transition rules in a certain order.
495
496
496
497
\subsubsection{2APL Configurations}
497
498
498
-
$$ A_{\iota} = \langle \iota, \sigma, \gamma, \Pi, \theta, \xi \rangle $$
499
+
The configuration of an individual agent consists of its \textbf{identifier}, \textbf{beliefs}, \textbf{goals}, \textbf{plans}, \textbf{substitutions that are resulted from queries to the belief and goal bases}, and the \textbf{received events}. Moreover, additional information is assigned to an agent's plan. In particular, a unique identifier is assigned to each plan which can be used to identify and repair failed plans. Also, the practical reasoning rules by means of which plans are generated are assigned to plans in order to avoid redundant applications of practical reasoning rules, e.g., to avoid generating multiple plans for one and the same goal.
500
+
501
+
\paragraph{Individual agent}
502
+
503
+
The configuration of an individual 2APL agent is defined as $ A_{\iota} = \langle \iota, \sigma, \gamma, \Pi, \theta, \xi \rangle $ where $\iota$ is a set of belief expressions representig the agent's identifier, $\sigma$ is a list of goals expressions representing the agent's belief base, $\gamma$ is the agent's goal base, $\Pi$ is a set of plan entries representing the agent's goal base, $\theta$ is a ground substitution that binds domain variables to gound terms, and $\xi = \langle E, I, M \rangle$ is the agent's event base, where
504
+
505
+
\begin{itemize}
506
+
\item $E$ is a set of events from the external environments, which has the form $event(A,S)$, where $A$ is a ground atom originated from the environment $S$.
507
+
\item $I$ is a set of plans identifiers denoting failed plans.
508
+
\item $M$ is the set of messages sent to the agent.
509
+
\end{itemize}
510
+
511
+
Each plan entry is a tuple $(\pi, r, p)$, where $\pi$ is the executing plan, $r$ is the instatation of the PG-rule throug which $\pi$ is generated, and $\p$ is the plan identifier. The belief base and each goal in the goal base are consistent as only positive atoms are used to represent them.
512
+
513
+
\paragraph{Multi-agents system}
514
+
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
+
499
517
500
518
\subsubsection{Transition rules for basic actions}
501
519
502
-
Skip action
520
+
\paragraph{Skip action}
503
521
$$ {{\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}}$$
504
522
505
-
Belief update action
523
+
\paragraph{Belief update action}
506
524
$$ {{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}} $$
507
525
508
-
Test action
526
+
\paragraph{Test action}
509
527
$$ {{( \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}} $$
510
528
511
529
512
-
Goal dynamics actions
530
+
\paragraph{Goal dynamics actions}
513
531
$$ {{{\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}} $$
514
532
515
533
$$ {{\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}} $$
516
534
517
535
518
-
Abstract action
536
+
\paragraph{Abstract action}
519
537
$$ {{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}} $$
520
538
521
-
Communication actions
539
+
\paragraph{Communication actions}
522
540
523
-
External actions
541
+
\paragraph{External actions}
524
542
525
543
526
544
\subsubsection{Transition rules for plans}
527
545
528
-
Sequence plan
546
+
\paragraph{Sequence plan}
529
547
$${ {\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}}$$
530
548
531
-
Conditional plan
549
+
\paragraph{Conditional plan}
532
550
$${ {(\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}}$$
533
551
\vskip 0.2ex
534
-
$${ {�\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}}$$
552
+
$${ {�\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}}$$
535
553
536
-
While plan
554
+
\paragraph{While plan}
537
555
$${ {(\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}}$$
538
556
\vskip 0.2ex
539
557
$${ {¬\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}}$$
540
558
541
-
Atomic plan
559
+
\paragraph{Atomic plan}
542
560
543
-
Multiple concurrent plans
544
-
561
+
\paragraph{Multiple concurrent plans}
545
562
546
563
\subsubsection{Practical reasoning rules}
547
564
548
-
Planing goal rules
565
+
\paragraph{Planing goal rules}
549
566
550
-
Procedure call rules
567
+
\paragraph{Procedure call rules}
551
568
552
-
Plan repair rules
569
+
\paragraph{Plan repair rules}
553
570
554
571
\subsubsection{Multi-agent transition rules}
555
572