Visualization of Temporal Logic Specifications

Abstract

The desired behaviour of a system can be formally specified using a temporal logic, and used to check whether a candidate design meets this specification, or to automatically design a system that does. Such techniques are in principle applicable to a wide range of types of systems, but their current extent of use does not fulfill their potential. One limitation has been the difficulty of writing and reading formal specifications. We present preliminary work on a visual method of viewing and editing specifications that is intended to address this challenge.