Enabling Automatic Certification of Online Auctions
This work addresses trust issues in agent-mediated e-commerce systems, though it is incremental as it builds on existing formal methods and semantic web technologies.
The paper tackled the problem of building trust in online auctions by enabling software agents to automatically verify desirable properties of auction mechanisms, achieving this by formalizing mechanisms in OWL-S and translating them to COQ for verification.
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.