PISAGOR: a proactive software agent for monitoring interactions

Abstract

E-commerce has become an integral part of everyday life. Many e-commerce systems enable users to browse products, place orders, and track deliveries online. However, these interactions is time-consuming, especially if they do not proceed as expected. Instead of a human user, software can offer automated support to monitor e-commerce transactions to ensure that they are completed by the businesses as planned. Accordingly, this paper studies methods to develop a software agent for monitoring its users’ interactions with businesses (PISAGOR). The interactions are represented as commitments, which have been extensively studied in multiagent systems. With a commitment-based specification at hand, the agent knows what the meaning of its interactions are and can therefore reason over its actions. The reasoning is accompanied with the as-good-as relation that compares the agent’s current state with its expectations from a transaction. This enables PISAGOR to decide whether the transaction is progressing as expected. Moreover, we propose operational rules for the agent to create expectations based on its commitments and check its progress toward them. We demonstrate via a case study how PISAGOR can detect if a user’s interactions are not progressing well and identify a problem for the user to take action.

Appendix

Theorem 1

$\Vvdash$relation is a preorder, i.e., it is reflexive, non-symmetric, and transitive.

Proof

It is trivial that $\Vvdash$is reflexive and non-symmetric. For atomic propositions, reflexivity follows from Axiom 1 and for commitments it follows from Axiom 4. For showing non-symmetry, any unidirectional edge in Fig. 5 serves as a counter-example for symmetry. Consider the edge between nodes 2 and 5. The proposition refurbished satisfies the violated base-level commitment $C^v$($\top$, refurbished), but the other direction is not true. The edges between nodes 6–7 and 1–6 show similar properties.

For transitivity, we need to show that if $\alpha$ $\Vvdash$ $\beta$ and $\beta$ $\Vvdash$ $\gamma$ then $\alpha$ $\Vvdash$ $\gamma$. Assume $\alpha$ is a proposition Con, $\beta$ and $\gamma$ are both base-level commitments with consequents Con. By Axiom 2, $\alpha$ $\Vvdash$ $\beta$, independently of the state of $\beta$. Now, when (1) the state of $\beta$ is fulfilled, by Axiom 4, $\beta$ $\Vvdash$ $\gamma$, independently of the state of $\gamma$. Then, $\alpha$ $\Vvdash$ $\gamma$, by Axiom 2. When (2) the state of $\beta$ is active, by Axiom 4, $\beta$ $\Vvdash$ $\gamma$, if the state of $\gamma$ is active or violated. Then, again $\alpha$ $\Vvdash$ $\gamma$, by Axiom 2. When (3) the state of $\beta$ is violated, by Axiom 4, $\beta$ $\Vvdash$ $\gamma$, if the state of $\gamma$ is also violated. Then, again $\alpha$ $\Vvdash$ $\gamma$, by Axiom 2. Thus, $\Vvdash$is transitive. Other combinations of $\alpha$, $\beta$ and $\gamma$ follow similarly. $\square$

Theorem 2

For an agent A, at time T, given a proposition Con, iff takeAction(A, T, Con).

Proof

We prove both directions by contradiction.

I. Forward direction (Completeness): If takeAction(A, T, Con), then .

Let $\exists Con$: takeAction(A, T, Con). Then, by Definition 8, either ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A))$ $=$ $\emptyset$, or $\exists$ x: x $\in$ ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A))$. First, consider the former case. Assume ${\mathcal {S}}^T(A)$ $\Vvdash$ ${\mathcal {S}}^T(A_p)$. This will occur only if ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A_p))$ $=$ $\emptyset$ also. Otherwise, a term that includes Con cannot be satisfied according to the satisfiability axioms. This is a contradiction, because, by Definition 8, ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A_p))$ cannot be empty.

Now, consider the latter case. Again, assume ${\mathcal {S}}^T(A)$ $\Vvdash$ ${\mathcal {S}}^T(A_p)$. There are three possibilities:

• 1. ${\mathcal {S}}^T(A_p)$ $=$ $\langle \emptyset$, $\emptyset \rangle$. Then, every state is as good as the empty state since there are no terms in it to satisfy (Definition 10). This is a contradiction, because, by Definition 8, ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A_p))$ cannot be empty.

• 2. ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A_p))$ $=$ $\emptyset$. Then, there is no need to satisfy a term that includes Con. This is a contradiction, because, again by Definition 8, ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A_p))$ cannot be empty.

• 3. $\exists$ y: y $\in$ ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A_p))$. Then, x is as good as y (since both are the terms that include Con). There are three possibilities:

  • (a) $x = Con$ or $x = C^f(Con)$. Then, according to the satisfiability axioms, x $\Vvdash$ y for any y. This is a contradiction, because, by Definition 8, u(x) cannot be greater than or equal to u(y).

  • (b) $x = C^a(Con)$ and ($y = C^a(Con)$ or $y = C^v(Con)$). Then, by Axiom 4, x $\Vvdash$ y. This is a contradiction, because, by Definition 8, u(x) cannot be greater than or equal to u(y).

  • (c) $x = C^v(Con)$ and $y = C^v(Con)$. Then, by Axiom 4, x $\Vvdash$ y. This is a contradiction, because, by Definition 8, u(x) cannot be equal to u(y).

Hence, we conclude that whenever the agent takes an action, .

II. Backward direction (Soundness): If , then $\exists Con$: takeAction(A, T, Con).

Let . Then, by Definition 10, $\exists$ y: y $\in$ ${\mathcal {S}}^T(A_p)$ and . That is, there is at least one term that is not satisfiable. Let y $\in$ ${\mathcal {T}}_{Con}({\mathcal {S}}^T(A_p))$. That is, Con be the proposition related to the term y (either y itself or the consequent of y in case y is a commitment). Now, assume takeAction(A, T, Con) does not hold. Then, $\exists$ x: x $\in$ ${\mathcal {S}}^T(A)$ and u(x) $\ge$ u(y). Otherwise, takeAction(A, T, Con) would hold. There are three possibilities:

• 1. $x = Con$ or $x = C^f(Con)$. Then, u(x) $\ge$ u(y) for any y, and no action needs to be taken. This is a contradiction, because, according to the satisfiability axioms x would be as good as any such y.

• 2. $x = C^a(Con)$ and ($y = C^a(Con)$ or $y = C^v(Con)$). Then, u(x) $\ge$ u(y), and no action needs to be taken. This is a contradiction, because, by Axiom 4, x would be as good as y.

• 3. $x = C^v(Con)$ and $y = C^v(Con)$. Then, u(x) $=$ u(y), and no action needs to be taken. This is a contradiction, because, by Axiom 4, x would be as good as y. $\square$