Model checking on timed-event structures

Abstract

We propose a new style of model checking of timed transition systems, where instead of reasoning about the timing of states with specific properties, we reason about the timings of events with specific properties. This shift in paradigm appears to be useful for verification of edge triggered control paths, where we are more interested in the timings of changes in signal values. We propose a temporal logic, event-triggered timed computation tree logic (ETCTL), which allows the specification of event properties such as posedge(signal) and negedge(signal) along with real time computation tree logic (RTCTL) properties. We show that all ETCTL properties are interval independent, that is, their truth can never change on states between successive events. By virtue of the interval independent property, reasoning about timings of events (using ETCTL) is more efficient computationally than reasoning about general timed properties. We present a labeling algorithm, and suggest extensions to automata theoretic and symbolic approaches.