Fully symbolic TCTL model checking for complete and incomplete real-time systems

• We use a symbolic formalism for real-time systems, called FSMT.
• We present a converter, able to transform timed automata into FSMTs.
• We present a fully symbolic full TCTL model checking algorithm for FSMTs.
• FSMTs can simulate parallelized interleaving semantics allowing parallelism of non-synchronising transitions.
• We extend our methods to incomplete real-time systems where part of the system is put into a black box.

In this paper we present a fully symbolic TCTL model checking algorithm for real-time systems represented in a formal model called finite state machine with time (FSMT), which works on fully symbolic state sets containing both the clock values and the state variables. Our algorithm is able to verify TCTL properties on complete and incomplete FSMTs containing unknown components. For that purpose over-approximations of state sets fulfilling a TCTL property ϕ for at least one implementation of the unknown components and under-approximations of state sets fulfilling ϕ for all possible implementations of the unknown components are computed. We present two different methods to convert timed automata to FSMTs. In addition to FSMTs simulating pure interleaving behaviour of timed automata we can produce FSMTs with a parallelized interleaving behaviour which allows parallelism of conflict-free transitions. This can dramatically reduce the number of steps during verification. Our prototype implementation outperforms the state-of-the-art model checkers UPPAAL and RED on complete systems, and on incomplete systems our tool is able to prove interesting properties when parts of the system are unknown.