We present a satisfiability-preserving translation of QTL formulae with counting modalities interpreted over finitely variable signals into formulae of the CLTL-over-clocks logic. The satisfiability of CLTL-over-clocks can be solved through a suitable encoding into the input logics of SMT solvers, so our translation constitutes an effective decision procedure for QTL with counting modalities. It is known that counting modalities increase the expressiveness of QTL (hence also of the expressively equivalent MITL logic); to the best of our knowledge, our decision procedure for such modalities is the first actually implemented.

Deciding Continuous-Time Metric Temporal Logic with Counting Modalities

BERSANI, MARCELLO MARIA;ROSSI, MATTEO GIOVANNI;SAN PIETRO, PIERLUIGI
2013-01-01

Abstract

We present a satisfiability-preserving translation of QTL formulae with counting modalities interpreted over finitely variable signals into formulae of the CLTL-over-clocks logic. The satisfiability of CLTL-over-clocks can be solved through a suitable encoding into the input logics of SMT solvers, so our translation constitutes an effective decision procedure for QTL with counting modalities. It is known that counting modalities increase the expressiveness of QTL (hence also of the expressively equivalent MITL logic); to the best of our knowledge, our decision procedure for such modalities is the first actually implemented.
Reachability Problems
9783642410352
9783642410369
Formal verification; Metric Temporal Logic; continuous time
File in questo prodotto:
File Dimensione Formato  
chp%3A10.1007%2F978-3-642-41036-9_8.pdf

Accesso riservato

: Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione 340.93 kB
Formato Adobe PDF
340.93 kB Adobe PDF   Visualizza/Apri

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/11311/758855
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 6
social impact