2-APL UPC project.
+64
-1
+64
-1
docs/2apl-doc.tex
+64
-1
docs/2apl-doc.tex
···
489
489
490
490
\subsection{Formal Semantics} %%%%%%% MARCOS HERE
491
491
492
-
Marcos here
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
+
494
+
%% TODO
495
+
496
+
\subsubsection{2APL Configurations}
497
+
498
+
$$ A_{\iota} = \langle \iota, \sigma, \gamma, \Pi, \theta, \xi \rangle $$
499
+
500
+
\subsubsection{Transition rules for basic actions}
501
+
502
+
Skip action
503
+
$$ {{\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
+
505
+
Belief update action
506
+
$$ {{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
+
508
+
Test action
509
+
$$ {{( \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
+
511
+
512
+
Goal dynamics actions
513
+
$$ {{{\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
+
515
+
$$ {{\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
+
517
+
518
+
Abstract action
519
+
$$ {{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
+
521
+
Communication actions
522
+
523
+
External actions
524
+
525
+
526
+
\subsubsection{Transition rules for plans}
527
+
528
+
Sequence plan
529
+
$${ {\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
+
531
+
Conditional plan
532
+
$${ {(\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
+
\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}}$$
535
+
536
+
While plan
537
+
$${ {(\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
+
\vskip 0.2ex
539
+
$${ {¬\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
+
541
+
Atomic plan
542
+
543
+
Multiple concurrent plans
544
+
545
+
546
+
\subsubsection{Practical reasoning rules}
547
+
548
+
Planing goal rules
549
+
550
+
Procedure call rules
551
+
552
+
Plan repair rules
553
+
554
+
\subsubsection{Multi-agent transition rules}
555
+
493
556
494
557
\section{2APL Platform}\label{sec:platform} %%%%%%% BORJA+MARCOS HERE
495
558