On-the-fly symbolic model checking for real-time systems

This paper presents an on-the-fly and symbolic algorithm for checking whether a timed automaton satisfies a formula of a timed temporal logic which is more expressive than TCTL. The algorithm is on-the-fly in the sense that the state-space is generated dynamically and only the minimal amount of information required by the verification procedure is stored in memory. The algorithm is symbolic in the sense that it manipulates sets of states, instead of states, which are represented as boolean combinationsof linear inequalities of clocks. We show how a prototype implementation of our algorithm has improved the performances of the tool KRONOS for the verification of the FDDI protocol.

• Type: Conference
• Year: 1997
• Where: RTSS
• Authors: Ahmed Bouajjani, Stavros Tripakis, Sergio Yovine
• Keywords: Algorithm, Control Systems, RTSS 1997, Symbolic Algorithm, Timed Temporal Logic