The recent advances in computer graphics and multimedia technology provide new means for the visualization of abstract information spaces through the use of multi-dimensional and multi-modal communication channels. In the context of computer-aided verification, this potential can be effectively employed to provide visual notations for mathematical formalisms. We describe a visual system which supports visual presentation and manipulation of temporal sequencing properties expressed in the formalism of computation tree logic. The system enforces a metaphoric transposition of the abstract temporal semantics of the logic onto a concrete visual space through the use of 3D graphics, multiple windowing, color associations, and through the joint and coherent exploitation of both textual and graphic representations. This results in a complex interaction environment supporting syntactic parsing, semantic understanding, and visual editing of temporal expressions.