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

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.
Lanotte, Ruggero; Maggiolo Schettini, A.; Troina, A.
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/1745888
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 3
social impact