Timed Diagnostics for Reachability Properties

We consider the problem of computing concrete diagnostics for timed automata and reachability properties. Concrete means containing information both about the discrete state changes and the exact amount of time passing at each state. Our algorithm solves the problem in O(l · n2 ) time, where l is the length of the diagnostic run and n the number of clocks. A prototype implementation in the tool Kronos has been used to produce a counter-example in the claimed-to-be-correct version of the collision detection protocol of [HSLL97].

• Type: Conference
• Year: 1999
• Where: TACAS
• Authors: Stavros Tripakis
• Keywords: Algorithms, Concrete Diagnostics, Discrete State Changes, Means Containing Information, TACAS 1999