Optimized Step Semantics Encoding for Bounded Model Checking of Timed Automata

To BMC of timed automata network, we present a novel time stamp semantics model for timed automata network with synchronization and shared variables, which allows not only mutually independent transitions but also dependent transitions to be compressed together between two states in succession. A key ingredient of our BMC encoding is the use of time stamp variables for shared variable accesses, which are overlooked in previous approaches. The proposed semantics represents the timed automata network in a significantly more compact way than previous step semantics, which allows maximally compressed steps of transitions and therefore is in this sense optimal. A preliminary experimental evaluation shows a significant performance improvement in the number of unrolling of BMC steps and run times as well.