Graphical tool for SC automata

Abstract

SC automata are a variation of timed automata which are closed under complementation. The major difference is SC automata have both history clocks which represent the time since some event occurred in the past and prophecy clocks which represent the time until some event occurs in the future. Humans have difficulty understanding and visualising the meaning of prophecy clocks and constraints which test their values. A graphical tool for constructing SC automata and experimenting with their accepting runs is presented. The tools emphasis is to provide understanding and visualising prophecy clocks rather than being a solid verifier. A simple evaluation of the tool is also presented.