Abstract
Whilst it can be highly desirable for software agents to engage in auctions, they are normally restricted to trading within known auctions, due to the complexity and heterogeneity of the auction rules within an e-commerce system. To allow for agents to deal with previously unseen protocols, we present a proof-carrying code approach using Coq wherein auction protocols can be specified and desirable properties be proven. This enables software agents to automatically certify claimed auction properties and assist them in their decision-making. We have illustrated our approach by specifying both the English and Vickrey auctions; have formalized different bidding strategies for agents; have certified that up to the valuation is the optimal strategy in English auction and truthful bidding is the optimal strategy in Vickrey auction for all agents. The formalization and certification are based on inductive definitions and constructions from within Coq. This work contributes to solving the problem of open societies of software agents moving between different institutions and seeking to make optimal decisions and will benefit those engaged in agent-mediated e-commerce.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Our Coq code is available upon request.
References
Berners-Lee, T., Hendler, J., Lassila, O., et al.: The semantic web. Sci. Am. 284(5), 28–37 (2001)
Necula, G.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106–119. ACM (1997)
The Coq Development Team: The coq proof assistant reference manual: Version 8.4 (2012) http://coq.inria.fr
Tadjouddine, E.M., Guerin, F.: Verifying dominant strategy equilibria in auctions. In: Burkhard, H.-D., Lindemann, G., Verbrugge, R., Varga, L.Z. (eds.) CEEMAS 2007. LNCS (LNAI), vol. 4696, pp. 288–297. Springer, Heidelberg (2007)
Tadjouddine, E., Guerin, F., Vasconcelos, W.: Abstractions for model-checking game-theoretic properties of auctions. In: Proceedings of the 7th International Joint Conference on Autonomous Agents and Multiagent Systems-Volume 3, International Foundation for Autonomous Agents and Multiagent Systems, pp. 1613–1616 (2008)
Tadjouddine, E.M.: Computational complexity of some intelligent computing systems. Int. J. Intell. Comput. Cybernetics 4(2), 144–159 (2011)
Tip, F.: A survey of program slicing techniques. J. Program. Lang. 3(3), 121–189 (1995)
Dolev, S., Panagopoulou, P., Rabie, M., Schiller, E., Spirakis, P.: Rationality authority for provable rational behavior. In: Proceedings of the 30th Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 289–290. ACM (2011)
Lapets, A., Levin, A., Parkes, D.: A typed language for truthful one-dimensional mechanism design. Technical report, Computer Science Department, Boston University (2008)
Sălcianu, A., Arkoudas, K.: Machine-checkable correctness proofs for intra-procedural dataflow analyses. Electr. Notes Theoret. Comput. Sci. 141(2), 53–68 (2005)
Dowek, G., Felty, A., Herbelin, H., Huet, G., Werner, B., Paulin-Mohring, C., et al.: The coq proof assistant user’s guide: Version 5.6 (1991)
Affeldt, R., Kobayashi, N.: Formalization and Verification of a Mail Server in Coq. In: Okada, M., Pierce, B., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 217–233. Springer, Heidelberg (2003)
Affeldt, R., Kobayashi, N., Yonezawa, A.: Verification of concurrent programs using the coq proof assistant: a case study. IPSJ Digital Courier 1(7), 117–127 (2005)
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)
Vestergaard, R.: A constructive approach to sequential nash equilibria. Inf. Process. Lett. 97(2), 46–51 (2006)
Cousot, P., Cousot, R.: Basic concepts of abstract interpretation. In: Jacquart, R. (ed.) Building the Information Society. IFIP, vol. 156, pp. 359–366. Springer, Heidelberg (2004)
Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. ACM SIGPLAN Not. 37(1), 178–190 (2002)
Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. ii. Oxford University Press, Oxford (1992)
Appel, A.: Foundational proof-carrying code. In: 16th Annual IEEE Symposium on Logic in Computer Science, Proceedings, pp. 247–256. IEEE (2001)
Fudenberg, D., Tirole, J.: Game Theory. MIT Press, Cambridge (1991)
Bellifemine, F., Caire, G., Greenwood, D.: Developing Multi-agent Systems with JADE (wiley series in agent technology). Wiley, Chichester (2007)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bai, W., Tadjouddine, E.M., Payne, T.R., Guan, S.U. (2014). A Proof-Carrying Code Approach to Certificate Auction Mechanisms. In: Fiadeiro, J., Liu, Z., Xue, J. (eds) Formal Aspects of Component Software. FACS 2013. Lecture Notes in Computer Science(), vol 8348. Springer, Cham. https://doi.org/10.1007/978-3-319-07602-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-07602-7_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07601-0
Online ISBN: 978-3-319-07602-7
eBook Packages: Computer ScienceComputer Science (R0)