Paper Info
Title
Runtime Verification: From Propositional To First-Order Temporal Logic
Abstract
Runtime Verification is a branch of formal methods concerned with analysis of execution traces for the purpose of determining the state or general quality of the executing system. The field covers numerous approaches, one of which is specification-based runtime verification, where execution traces are checked against formal specifications. The paper presents syntax, semantics, and monitoring algorithms for respectively propositional and first-order temporal logics. In propositional logics the observed events in the execution trace are represented using atomic propositions, while first-order logic allows universal and existential quantification over data occurring as arguments in events. Monitoring of the first-order case is drastically more challenging than the propositional case, and we present a solution for this problem based on BDDs. We furthermore discuss monitorability of temporal properties by dividing them into different classes representing different degrees of monitorability.
Year
DOI
Venue
2018
10.1007/978-3-030-03769-7_7
RUNTIME VERIFICATION (RV 2018)
Field
DocType
Volume
Existential quantification,Computer science,Atomic sentence,Theoretical computer science,Runtime verification,Formal specification,Temporal logic,Formal methods,Syntax,Semantics
Conference
11237
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
12
2
Name
Order
Citations
PageRank
Klaus Havelund13522254.55
Doron Peled23357273.18