Paper Info
Title
An Extension Of First-Order Ltl With Rules With Application To Runtime Verification
Abstract
Linear temporal logic (LTL) is extensively used in formal methods, in particular in runtime verification (RV) and in model checking. Its propositional version was shown by Wolper (1983, Inform Control 56(1/2): 72-99) to be limited in expressiveness. Several extensions of propositional LTL, which promote the expressive power to that of Buchi automata, have therefore been proposed; however, none of those, by and large, have been adopted for formal methods. We present an extension of propositional LTL with rules, that is as expressive as these aforementioned extensions. We then show a similar deficiency in the expressiveness of first-order LTL and present an extension of it with rules, which parallels the propositional version. In our work on runtime verification, we focus on execution traces which consist of events that carry data, where a first-order version of LTL is needed, and in particular on past time versions of first-order LTL. In the previous work, we provided an algorithm for past time first-order LTL that uses BDDs to represent relations over data elements, and implemented it as a tool called DejaVu. In this paper, we propose a monitoring algorithm for the extension of past time first-order LTL with rules. This is implemented as an extension of DejaVu, and experimental results are provided.
Year
DOI
Venue
2021
10.1007/s10009-021-00626-y
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
Keywords
DocType
Volume
Runtime-verification, Linear temporal logic, Binary decision diagrams
Journal
23
Issue
ISSN
Citations 
4
1433-2779
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
K. Havelund110914.14
Doron Peled23357273.18