Binding telecooperation - a formal model for electronic commerce

This paper formally defines the concept "electronic contract" and identifie s its "goals", "obligations" and "binding phase". The definitions obtained here are used first for the specification of electronic contracts and secon dly for the verification of local implementations of electronic cooperation contracts. The local representation of contracts and the communication bet ween them, multiple and overlapping runs through a binding phase and the ro le of proofs are treated separately. The definitions are based on the theor y of formal languages and automata. They are demonstrated by a simple examp le of a bilateral offer-order-deliver-pay cooperation. (C) 2001 Elsevier Sc ience B.V. All rights reserved.