Verification of Relational Transducers for Electronic Commerce Marc Spielmann   View Paper (PDF)   Return to Award Talks Abstract Motivated by recent work of Abiteboul, Vianu, Fordham, and Yesha [3] we investigate the verifiability of transaction protocols specifying the interaction of multiple partiesvia a network, where each party is equipped with an (active) database that participates in the interaction. Such transaction protocols typically occur in the context of electronic commerce applications and can be formalized as relational transducers. We introduce a class of powerful relational transducers based on Gurevich's abstract state machines and show that several verification problems related to electronic commerce applications can be solved for these transducers. Our approach is, in some sense, complementary to the approach in [3]. References Note: References link to DBLP on the Web. [1] Serge Abiteboul , Laurent Herr , Jan Van den Bussche : Temporal Versus First-Order Logic to Query Temporal Databases. PODS 1996 : 49-57 [2] Serge Abiteboul , Richard Hull , Victor Vianu : Foundations of Databases. Addison-Wesley 1995, ISBN 0-201-53771-0 Contents [3] Serge Abiteboul , Victor Vianu , Bradley S. Fordham , Yelena Yesha : Relational Transducers for Electronic Commerce. PODS 1998 : 179-187 [4] ... [5] ... [6] Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov : Complexity and Expressive Power of Logic Programming. IEEE Conference on Computational Complexity 1997 : 82-101 [7] ... [8] E. Allen Emerson : Temporal and Modal Logic. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) 1990 : 995-1072 [9] Bradley S. Fordham , Serge Abiteboul , Yelena Yesha : Evolving Databases: An Application to Electronic Commerce. IDEAS 1997 : 191-200 [10] Georg Gottlob , Gerti Kappel , Michael Schrefl : Semantics of Object-Oriented Data Models - The Evolving Algebra Approach. East/West Database Workshop 1990 : 144-160 [11] ... [12] ... [13] Neil Immerman , Moshe Y. Vardi : Model Checking and Transitive-Closure Logic. CAV 1997 : 291-302 [14] Alon Y. Levy , Inderpal Singh Mumick , Yehoshua Sagiv , Oded Shmueli : Equivalence, Query-Reachability, and Satisfiability in Datalog Extensions. PODS 1993 : 109-122 [15] Philippe Picouet , Victor Vianu : Semantics and Expressiveness Issues in Active Databases. JCSS 57(3) : 325-355(1998) [16] ... [17] ... [18] Marc Spielmann : Automatic Verification of Abstract State Machines. CAV 1999 : 431-442 [19] Moshe Y. Vardi : The Complexity of Relational Query Languages (Extended Abstract). STOC 1982 : 137-146 [20] Moshe Y. Vardi : On the Complexity of Bounded-Variable Queries. PODS 1995 : 266-276 BIBTEX @inproceedings{DBLP:conf/pods/Spielmann00,   author    = {Marc Spielmann},    title     = {Verification of Relational Transducers for Electronic Commerce},    booktitle = {Proceedings of the Nineteenth ACM SIGMOD-SIGACT-SIGART Symposium                 on Principles of Database Systems, May 15-17, 2000, Dallas, Texas,                 USA},    publisher = {ACM},    year      = {2000},    isbn      = {1-58113-214-X},    pages     = {92-103},    crossref  = {DBLP:conf/pods/00},    bibsource = {DBLP, http://dblp.uni-trier.de} } }, DiSC'01 Copyright ©2002 ACM Inc.