Explainable Online Monitoring of Metric First-Order Temporal Logic

被引：2

作者：

Lima, Leonardo ^{[1
]}

Huerta y Munive, Jonathan Julian ^{[1
]}

Traytel, Dmitriy ^{[1
]}

机构：

[1] Univ Copenhagen, Dept Comp Sci, Copenhagen, Denmark

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2024 | 2024年 / 14570卷

关键词：

D O I：

10.1007/978-3-031-57246-3_16

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Metric first-order temporal logic (MFOTL) is an expressive formalism for specifying temporal and data-dependent constraints on streams of time stamped, data-carrying events. It serves as the specification language of several runtime monitors. These monitors input an MFOTL formula and an event stream prefix and output satisfying assignments to the formula's free variables. For complex formulas, it may be unclear why a certain assignment is output. We propose an approach that accompanies assignments with detailed explanations, in the form of proof trees. We develop a new monitor that outputs such explanations. Our tool incorporates a formally verified checker that certifies the explanations and a visualization that allows users to interactively explore and understand the outputs.

引用

页码：288 / 307

页数：20

共 50 条

[21] Nonclausal deduction in first-order temporal logic
Abadi, Martin, 1600, (37):
[22] Equality and monodic first-order temporal logic
Degtyarev A.
Fisher M.
Lisitsa A.
Studia Logica, 2002, 72 (2) : 147 - 156
[23] Proof planning for first-order temporal logic
Castellini, C
Smaill, A
AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 235 - 249
[24] First-order logic with two variables and unary temporal logic
Etessami, K
Vardi, MY
Wilke, T
INFORMATION AND COMPUTATION, 2002, 179 (02) : 279 - 295
[25] First-order logic with two variables and unary temporal logic
Etessami, K
Vardi, MY
Wilke, T
12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, : 228 - 235
[26] THE FIRST-ORDER LOGIC OF CZF IS INTUITIONISTIC FIRST-ORDER LOGIC
Passmann, Robert
JOURNAL OF SYMBOLIC LOGIC, 2024, 89 (01) : 308 - 330
[27] First-Order Logic and First-Order Functions
Freire, Rodrigo A.
LOGICA UNIVERSALIS, 2015, 9 (03) : 281 - 329
[28] A Benchmark Generator for Online First-Order Monitoring
Krstic, Srdan
Schneider, Joshua
RUNTIME VERIFICATION (RV 2020), 2020, 12399 : 482 - 494
[29] Monitoring of temporal first-order properties with aggregations
Basin, David
Klaedtke, Felix
Marinovic, Srdjan
Zalinescu, Eugen
FORMAL METHODS IN SYSTEM DESIGN, 2015, 46 (03) : 262 - 285
[30] Monitoring of temporal first-order properties with aggregations
David Basin
Felix Klaedtke
Srdjan Marinovic
Eugen Zălinescu
Formal Methods in System Design, 2015, 46 : 262 - 285

← 1 2 3 4 5 →