Visual Specification of Branching Time Temporal Logic

Alberto Del Bimbo,  Luigi Rella,  Enrico Vicario  

 About the Authors

Visual Formalism   Visual Specification Languages   Temporal Logic   3D Visualization  


Branching time Temporal Logic is a descriptive language for the specification of ordering relationships characterizing the execution sequencing of time-varying systems. A considerable work has been done around this model, but its acceptance within industrial contexts is still hurdled by the asperity of its notation. A visual language is presented which overcomes this hurdle by embedding the formal nucleus of Temporal Logic within a visual shell. Matching the recursive syntax of the underlying mathematical notation, thevisual formalism is defined through a set of recursive visualization rules, which yield a generative approach to the visualization of any generic textual formula. A system is also presented which exploits the visual formalism to provide a graphic representation of branching time formulae within a 3D virtual space. The system supports an intuitive understanding of the meaning of complex formulae by providing a concrete representation for each of the three inherent dimensions of branching time formulae: time, parallelism and nesting.

 Document in PostScript (compressed, 334188 bytes)

Visual Programming with Graph Rewriting Systems ViTABaL: A Visual Language Supporting Design by Tool Abstraction Index of Talks Proceedings - 11th Intl. Symposium on Visual Languages