Verification of Relational Transducers for Electronic Commerce

Yesha, we investigate the verifiability of transaction protocols
specifying the interaction of multiple parties via a network.
The transaction protocols which we are concerned with 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 are decidable for
our class of relational transducers.