Verification of Relational Transducers For Electronic Commerce

Motivated by recent work of Abiteboul, Vianu, Fordham, and Yesha [3] we investigate the verifiability of transaction protocols specifying the interaction of multiple parties via 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]