In this paper, a formal basis for multimedia collaborations is proposed. The formal basis establishes a precise mathematical framework for supporting a wide spectrum of structured collaborative tasks, ranging from simple meetings and conferences to classrooms and examinations, and from corporate negotiations, work flow tasks, and team design endeavors to courtroom hearings. We mechanize three levels of abstraction: streams at the lowest level, for media communication, sessions at the next level, which represent collections of semantically related media streams, and conferences, which represent temporally related sequences of sessions. The mathematical framework has been mechanized in Prototype Verification System (PVS) from SRI International. The mechanization allows us to experiment with different formal models, and reason about properties of multimedia collaborations efficiently. The mechanized framework supports unification of both interactive and non-interactive collaborations, sophisticated access control and intra-group and inter-group collaborations, yielding a powerful set of building blocks for constructing multimedia applications. A formal specification of collaborations can form the basis of a transformational approach to automatically synthesize low-level, network environment specific constraints, necessary for managing media communication in multimedia collaborations. A prototype collaboration management system based on the framework has been implemented at the UCSD Multimedia Laboratory.

• icmcs95.ps