@inproceedings{13de124832424ddbbb07e60d4d68965d,
title = "MLTL benchmark generation via formula progression",
abstract = "Safe cyber-physical system operation requires runtime verification (RV), yet the burgeoning collection of RV technologies remain comparatively untested due to a dearth of benchmarks with oracles enabling objectively evaluating their performance. Mission-time LTL (MLTL) adds integer temporal bounds to LTL to intuitively describe missions of such systems. An MLTL benchmark for runtime verification is a 3-tuple consisting of (1) an MLTL specification ϕ; (2) a set of finite input streams representing propositional system variables (call this computation π) over the alphabet of ϕ; (3) an oracle stream of 〈v, t〉 pairs where verdict v is the result (true or false) for time t of evaluating whether πt |= ϕ (computation π at time t satisfies formula ϕ). We introduce an algorithm for reliably generating MLTL benchmarks via formula progression. We prove its correctness, demonstrate it executes efficiently, and show how to use it to generate a variety of useful patterns for the evaluation and comparative analysis of RV tools.",
author = "Jianwen Li and Rozier, \{Kristin Y.\}",
note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2018.; 18th International Conference on Runtime Verification, RV 2018 ; Conference date: 10-11-2018 Through 13-11-2018",
year = "2019",
doi = "10.1007/978-3-030-03769-7\_25",
language = "英语",
isbn = "9783030037680",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "426--433",
editor = "Christian Colombo and Martin Leucker",
booktitle = "Runtime Verification- 18th International Conference, RV 2018, Proceedings",
address = "德国",
}