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 条

[31] On Finite Domains in First-Order Linear Temporal Logic
Kuperberg, Denis
Brunel, Julien
Chemouil, David
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 : 211 - 226
[32] Axiomatizing the monodic fragment of first-order temporal logic
Wolter, F
Zakharyaschev, M
ANNALS OF PURE AND APPLIED LOGIC, 2002, 118 (1-2) : 133 - 145
[33] Monitoring of Temporal First-Order Properties with Aggregations
Basin, David
Klaedtke, Felix
Marinovic, Srdjan
Zalinescu, Eugen
RUNTIME VERIFICATION, RV 2013, 2013, 8174 : 40 - 58
[34] Decidable Cases of First-order Temporal Logic with Functions
Walter Hussak
Studia Logica, 2008, 88 (2) : 247 - 261
[35] A COMPLETENESS THEOREM OF FIRST-ORDER TEMPORAL LOGIC WITH EQUALITY
唐同诰
Science China Mathematics, 1985, (05) : 532 - 540
[36] The power of the ''always'' operator in first-order temporal logic
Kaminski, M
Wong, CK
THEORETICAL COMPUTER SCIENCE, 1996, 160 (1-2) : 271 - 281
[37] An Axiomatization of a First-order Branching Time Temporal Logic
Doder, Dragan
Ognjanovic, Zoran
Markovic, Zoran
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2010, 16 (11) : 1439 - 1451
[38] First Order Temporal Logic Monitoring with BDDs
Havelund, Klaus
Peled, Doron
Ulus, Dogan
PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), 2017, : 116 - 123
[39] A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Basin, David
Dardinier, Thibault
Heimes, Lukas
Krstic, Srdan
Raszyk, Martin
Schneider, Joshua
Traytel, Dmitriy
AUTOMATED REASONING, PT I, 2020, 12166 : 432 - 453
[40] The formal specification and implementation of a modest first-order temporal logic
Sachdev, S
Trudel, A
INTELLIGENT PROBLEM SOLVING: METHODOLOGIES AND APPROACHES, PRODEEDINGS, 2000, 1821 : 443 - 452

← 1 2 3 4 5 →