Semantics and Runtime Monitoring of TLCharts: Statechart Automata with Temporal Logic Conditioned Transitions

This paper describes the semi-formal semantics and a run-time monitoring technique for TLCharts, a visual specification language that combines the visual and intuitive appeal of non-deterministic Harel Statecharts with formal specifications written in Linear-time (Metric) Temporal Logic (LTL and MTL). We describe an automata-theoretic semantics for non-deterministic statecharts with negation and state overlapping and extend it to cater for temporally annotated transitions, thereby providing a simple automata theoretic semantics for TLCharts. We also describe a run-time monitoring technique for TLCharts.