Systems ofData 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
LANOTTE, RUGGERO;
2010-01-01
Abstract
Systems ofData 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.File | Dimensione | Formato | |
---|---|---|---|
lanotte_acta.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
DRM non definito
Dimensione
716.83 kB
Formato
Adobe PDF
|
716.83 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.