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 / Bozzelli, L.; Murano, A.; Peron, A.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 283:(2022), p. 104673. [10.1016/j.ic.2020.104673]
Context-free timed formalisms: Robust automata and linear temporal logics
Bozzelli L.;Murano A.;Peron A.
2022
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 | Dimensione | Formato | |
---|---|---|---|
Contextfree-timed-formalisms-Robust-automata-and-linear-temporal-logics2020Information-and-Computation(1).pdf
non disponibili
Descrizione: Articolo principale
Tipologia:
Documento in Pre-print
Licenza:
Accesso privato/ristretto
Dimensione
1.16 MB
Formato
Adobe PDF
|
1.16 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.