Logo del repository
  1. Home
 
Opzioni

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

Bozzelli L.
•
Murano A.
•
Peron A.
2022
  • journal article

Periodico
INFORMATION AND COMPUTATION
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.
DOI
10.1016/j.ic.2020.104673
WOS
WOS:000754556900003
Archivio
https://hdl.handle.net/11368/3032321
info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85098165938
https://www.sciencedirect.com/science/article/pii/S0890540120301668?via=ihub
Diritti
open access
license:copyright editore
license:creative commons
license uri:iris.pri02
license uri:http://creativecommons.org/licenses/by-nc-nd/4.0/
Soggetti
  • Metric temporal logic...

  • Model checking

  • Temporal logic

  • Timed automata

google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback