Mcta: heuristics and search for timed systems. Mcta is a directed model checking tool for concurrent systems of timed automata. This paper reviews Mcta and its new developments from an implementation point of view. The new developments include both heuristics and search techniques that define the state of the art in directed model checking. In particular, Mcta features the powerful class of pattern database heuristics for efficiently finding shortest possible error traces. Furthermore, Mcta offers new search techniques based on multi-queue search algorithms. Our evaluation demonstrates that Mcta is able to significantly outperform previous versions of Mcta as well as related state-of-the-art tools like Uppaal and Uppaal/Dmc.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.