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.
Reachability results for timed automata with unbounded data structures / Ruggero Lanotte; Andrea Maggiolo-Schettini; Angelo Troina. - In: ACTA INFORMATICA. - ISSN 0001-5903. - STAMPA. - 47:5(2010), pp. 279-311. [10.1007/s00236-010-0121-8]
Reachability results for timed automata with unbounded data structures
TROINA, ANGELO
2010
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.