This site is accompanying the Science of Computer Programming submission of the paper with the title Fully Symbolic TCTL Model Checking for Complete and Incomplete Timed Systems.
On this site you can find descriptions of the benchmarks used in the paper and the complete tables of the results.
The following benchmark descriptions show the benchmark as timed automaton. Each model checker (fsmtMC, uppaal, red and kronos) reads the benchmark in his own file type. Our tool fsmtMC uses a symbolic model called finite state machine with time (FSMT) which is produced based on a timed automaton.
In the following you will find the complete results from the experiments conducted for this paper. They include the conversion times needed for the translation from timed automata into FSMTs for both configurations, pure interleaving (ta2fsmt-inter) and parallelized interleaving (ta2fsmt-para). In order to produce incomplete FSMTs the converter has to produce different transition functions and reset conditions computed in three seperate runs, considering transitions which do not synchronize with the black box (no-sync), urgent transitions which syncronize with the black box (u-sync) and all transitions (all).
The run times include time for the competitors uppaal (UPPAAL), red (RED) and kronos (KRONOS). For our tool fsmtMC we give the times on FSMTs simulating pure interleaving behaviour (fsmtMC-inter) and on FSMTs simulating parallelized interleaving behaviour (fsmtMC-para). Additionally to the times we give the number of discrete steps (disc) and the number of continuous steps (cont) needed. On incomplete FSMTs the column (BB-inter) gives the result on FSMTs with pure interleaving behaviour and the column (BB-para) gives the times of the model checker run on FSMTs with parallelized interleaving behaviour.