Reachability results for timed automata with unbounded data structures

Systems of Data Management Timed Automata (SDMTAs) are networks of communicating timed automata with structures to store messages and functions to manipulate them. We prove the decidability of the reachability problem for a subclass of SDMTAs which assumes an unbounded knowledge, and we analyze the expressiveness of the model and the considered subclass. In particular, while SDMTAs can simulate a Turing machine, and hence the reachability problem is in general undecidable, the subclass for which reachability is decidable, when endowed with a concept of recognized language, accepts languages that are not regular. As an application, we model and analyze a variation of the Yahalom protocol.