Author(s):

Elgyutt, Adrian; Ferrère, Thomas; Henzinger, Thomas A

Title: 
Monitoring temporal logic with clock variables

Title Series: 
LNCS

Affiliation 
IST Austria 
Abstract: 
We solve the offline monitoring problem for timed propositional temporal logic (TPTL), interpreted over densetime Boolean signals. The variant of TPTL we consider extends linear temporal logic (LTL) with clock variables and reset quantifiers, providing a mechanism to specify realtime constraints. We first describe a general monitoring algorithm based on an exhaustive computation of the set of satisfying clock assignments as a finite union of zones. We then propose a specialized monitoring algorithm for the onevariable case using a partition of the time domain based on the notion of region equivalence, whose complexity is linear in the length of the signal, thereby generalizing a known result regarding the monitoring of metric temporal logic (MTL). The region and zone representations of time constraints are known from timed automata verification and can also be used in the discretetime case. Our prototype implementation appears to outperform previous discretetime implementations of TPTL monitoring,

Conference Title:

FORMATS: Formal Modeling and Analysis of Timed Systems

Volume: 
11022

Conference Dates:

September 4  6, 2018

Conference Location:

Beijing, China

ISBN:

9783030001506

Publisher:

Springer

Date Published:

20180826

Start Page: 
53

End Page:

70

DOI: 
10.1007/9783030001513_4

Open access: 
no 