aamas 2004

SOCS-SI demo storyboard

Contacts:

Marco Alberti, Ph. D. Student

Federico Chesani, Ph. D. Student

Paolo Torroni, Ph. D.

 

This page illustrates a storyboard of the SOCS-SI demo to be presented at AAMAS 2004. The examples are based on the "first price sealed bid" auction, whose protocol definition is presented later in this page.

We are going to present two different scenarios: in the first scenario the protocol is satisfied, and the SOCS-SI tool communicates the successful verification of the interaction (screenshots 1-4). In the second scenario, instead, the auctioneer forgets to notify some bidders that they have lost. When the auction terminates, the SOCS-SI detects this violation of the protocol (screenshots 5-6).

 

Scenario 1:The SOCS-SI tool has read from a file the list of messages, and it is ready to elaborate them.
  The auctioneer (named f) has opened an auction, and three bidders (taxi1, taxi2, taxi3) have placed a bid. The screenshot illustrates a possible set of expectations: f is expected to tell to taxi1 it has won the auction, and to tell to the others they have lost the auction (expectations are highlighted in blue).
  The auctioneer agent has behaved properly, and the expectations have been fullfilled.
  If we communicate to the SOCS-SI tool that no more messages can arrive, then the SOCS-SI tool declares the successful verification of the interaction (successful here means that all of the participants to the auction have complied to the auction protocol).
  Scenario 2: As in the screenshot no. 2, the auctioner has opened an auction and some taxis have placed a bid. Expectations have been generated...
  In this case, the auctioneer has not notified taxi2 and taxi3 that they have lost the auction... the protocol has not been respected!

 

The auction protocol

Here we present the auction protocol in terms of the Social Integrity Constraints that should be satisfied in order for the protocol to be fulfilled

IC1:

H(tell(B,A,bid(Item,Quote),AuctionId),TBid)
--->
E(tell(A,B,openauction(Item,TEnd,TDeadline),AuctionId),TOpen)
/\ TOpen < TBid
/\ TBid <= TEnd
/\ TEnd < TDeadline.

It asserts that if a bidder B has placed a bid at time TBid, an auctioneer A is expected to have opened the auction at a previous time TOpen.

 

IC2:

H(tell(A,B,openauction(Item,TEnd,TDeadline),AuctionId),TOpen)
/\ H(tell(B,A,bid(Item,Quote),AuctionId),TBid)
/\ TOpen < TBid
/\ TOpen <= TEnd
/\ TEnd < TDeadline
--->
E(tell(A,B,answer(win,Item,Quote),AuctionId),TWin)
/\ TWin <= TDeadline/\ TEnd < TWin
\/
E(tell(A,B,answer(lose,Item,Quote),AuctionId),TLose)
/\ TLose <= TDeadline
/\ TEnd < TLose.

For each bidder B that placed a bid at the time TBid, the auctioneer A should notify B that it has either won or lost.

 

IC3:

H(tell(A,B,answer(win,Item,Quote),AuctionId),TWin)
--->
EN(tell(A,B,answer(lose,Item,Quote),AuctionId),TLose)
/\ TLose > TWin.

IC4:

H(tell(A,B,answer(lose,Item,Quote),AuctionId),TLose)
--->
EN(tell(A,B,answer(win,Item,Quote),AuctionId),TWin)
/\ TWin > TLose.

If auctioneer A has notified bidder B that it has won the auction, A is expected not to notify B of having lost the auction afterwards, and vice-versa.

Scenario 1

In the first scenario, the auctioneer f opens an auction for getting a taxi at the lowest price available. Three taxis, taxi1, taxi2 and taxi3, place a bid. The auctioneer f chooses the cheapest bid, and communicates to the other agents that they have lost the auction. The exchanged messages are the following:

tell( auction1, f, taxi1, openauction, [taxiToStation,10,20], 5).
tell( auction1, f, taxi2, openauction, [taxiToStation,10,20], 5).
tell( auction1, f, taxi3, openauction, [taxiToStation,10,20], 5).
tell( auction1, taxi1, f, bid, [taxiToStation,3], 7).
tell( auction1, taxi2, f, bid, [taxiToStation,5], 8).
tell( auction1, taxi3, f, bid, [taxiToStation,7], 9).
tell( auction1, f, taxi1, answer, [win, taxiToStation,3], 12).
tell( auction1, f, taxi2, answer, [lose,taxiToStation,5], 13).
tell( auction1, f, taxi3, answer, [lose,taxiToStation,7], 14).

 

Scenario 2

The second scenario is quite similar to the first one, with the difference that the auctioneer f communicates to taxi1 that it has won the auction, but it does not tell the others that they have lost:

tell( auction1, f, taxi1, openauction, [taxiToStation,10,20], 5).
tell( auction1, f, taxi2, openauction, [taxiToStation,10,20], 5).
tell( auction1, f, taxi3, openauction, [taxiToStation,10,20], 5).
tell( auction1, taxi1, f, bid, [taxiToStation,3], 7).
tell( auction1, taxi2, f, bid, [taxiToStation,5], 8).
tell( auction1, taxi3, f, bid, [taxiToStation,7], 9).
tell( auction1, f, taxi1, answer, [win, taxiToStation,3], 12).

This work is partially funded by the Information Society Technologies programme of the European Commission under the IST-2001-32530 project.