Enabling Automatic Certification of Online Auctions

We consider the problem of building up trust in a network of online auctions by software agents. This requires agents to have a deeper understanding of auction mechanisms and be able to verify desirable properties of a given mechanism. We have shown how these mechanisms can be formalised as semantic web services in OWL-S, a good enough expressive machine-readable formalism enabling software agents, to discover, invoke, and execute a web service. We have also used abstract interpretation to translate the auction's specifications from OWL-S, based on description logic, to COQ, based on typed lambda calculus, in order to enable automatic verification of desirable properties of the auction by the software agents. For this language translation, we have discussed the syntactic transformation as well as the semantics connections between both concrete and abstract domains. This work contributes to the implementation of the vision of agent-mediated e-commerce systems.