An Extended Temporal Logic for CSCW
Costas Papadopoulos · The Computer Journal · 2002
Computer supported cooperative work (CSCW) poses new challenges that require the development of novel formal methods. For example, the synchronous collaboration of multiple users under strict timing constraints requires formal methods that can represent timing properties. In this paper, it is argued that temporal logic can be sufficiently expressive to specify such properties of CSCW. In particular, groupware temporal logic (GTL) has been developed as an extension of computation tree logic, to enable the specification of timing properties that characterize CSCW. The utility of GTL is demonstrated with several examples from CSCW, including cooperation in a virtual environment and the use of a shared text editor. The possibility of verifying CSCW systems with model checking is also examined, focusing particularly on a cooperative design toolkit.