The paper focuses on automata and linear temporal logics for real-time pushdown reactive systems bridging tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though preserving tractability. As for automata, we introduce Event-Clock Nested Automata (ECNA), a formalism that combines Event Clock Automata (ECA) and Visibly Pushdown Automata (VPA). ECNA enjoy the same closure and decidability properties of ECA and VPA expressively extending any previous attempt of combining ECA and VPA. As for temporal logics, we introduce two formalisms for specifying quantitative timing context-free requirements: Event-Clock Nested Temporal Logic (EC_NTL) and Nested Metric Temporal Logic (NMTL). EC_NTL is an extension of both the logic CaRet and Event-Clock Temporal Logic having EXPTIME-complete satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Systems (VPTS) against EC_NTL. NMTL is a context-free extension of standard Metric Temporal Logic (MTL) which is in general undecidable having, though, a fragment expressively equivalent to EC_NTL with EXPTIME-complete satisfiability and visibly model-checking of VPTS problems.

Context-free timed formalisms: Robust automata and linear temporal logics

Peron A.
2022-01-01

Abstract

The paper focuses on automata and linear temporal logics for real-time pushdown reactive systems bridging tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though preserving tractability. As for automata, we introduce Event-Clock Nested Automata (ECNA), a formalism that combines Event Clock Automata (ECA) and Visibly Pushdown Automata (VPA). ECNA enjoy the same closure and decidability properties of ECA and VPA expressively extending any previous attempt of combining ECA and VPA. As for temporal logics, we introduce two formalisms for specifying quantitative timing context-free requirements: Event-Clock Nested Temporal Logic (EC_NTL) and Nested Metric Temporal Logic (NMTL). EC_NTL is an extension of both the logic CaRet and Event-Clock Temporal Logic having EXPTIME-complete satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Systems (VPTS) against EC_NTL. NMTL is a context-free extension of standard Metric Temporal Logic (MTL) which is in general undecidable having, though, a fragment expressively equivalent to EC_NTL with EXPTIME-complete satisfiability and visibly model-checking of VPTS problems.
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0890540120301668-main.pdf

Accesso chiuso

Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 965.72 kB
Formato Adobe PDF
965.72 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
1-s2.0-S0890540120301668-main-Post_print.pdf

Open Access dal 17/11/2023

Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Creative commons
Dimensione 1.51 MB
Formato Adobe PDF
1.51 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

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/11368/3032321
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact