Abstractions for model checking of event timings

Verification of timed temporal properties of a circuit is a computationally complex problem both in terms of space and time. In this paper we study different abstractions of timed systems and the temporal logics which are preserved under these abstractions. In particular we show that while known timed logics such as RTCTL and TCTL are preserved by bisimulation equivalence, the timings of events (signal changes) are preserved in a more compact abstraction. Experimental results show that this abstraction requires significantly less space and is competitive in terms of time required for verification