We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLfMT), a
recently introduced extension of LTL over finite traces (LTLf) where
propositions are replaced by first-order formulas and where first-order
variables referring to different time points can be compared. In general,
LTLfMT was shown to be semi-decidable for any decidable first-order theory
(e.g., linear arithmetics), with a tableau-based semi-decision procedure.
In this paper we present a sound and complete pruning rule for the LTLfMT
tableau. We show that for any LTLfMT formula that satisfies an abstract,
semantic condition, that we call finite memory, the tableau augmented with the
new rule is also guaranteed to terminate. Last but not least, this technique
allows us to establish novel decidability results for the satisfiability of
several fragments of LTLfMT, as well as to give new decidability proofs for
classes that are already known.

本文研究了线性时间逻辑模块理论在有限轨迹上的应用，其中命题使用一阶公式替代，并且可以比较不同时间点引用的一阶变量。我们提出了一种用于 LTLfMT 表格的完备且有效的修剪规则，该规则在满足有限内存的抽象语义条件的任何 LTLfMT 公式下，通过增加新规则可以保证表格也能终止。最重要的是，这种技术使我们能够建立关于 LTLfMT 的多个片段可满足性的新的可判定性结果，并对已知类别给出新的可判定性证明。

LTLf 模块化理论的决定性片段（扩展版）

Decidable Fragments of LTLf Modulo Theories (Extended Version)

Temporal logics over finite traces have recently seen wide application in a
number of areas, from business process modelling, monitoring, and mining to
planning and decision making. However, real-life dynamic systems contain a
degree of uncertainty which cannot be handled with classical logics. We thus
propose a new probabilistic temporal logic over finite traces using
superposition semantics, where all possible evolutions are possible, until
observed. We study the properties of the logic and provide automata-based
mechanisms for deriving probabilistic inferences from its formulas. We then
study a fragment of the logic with better computational properties. Notably,
formulas in this fragment can be discovered from event log data using
off-the-shelf existing declarative process discovery techniques.

提出了一种新的基于超定理解的概率时态逻辑，用于处理现实动态系统中的不确定性，探讨了逻辑的特性并提供了基于自动机的推断机制。同时，研究了具有更好计算性质的逻辑片段，可以通过现有的声明性流程发现技术从事件日志数据中发现公式。

关于带不确定性有限轨迹的时间逻辑（技术报告）

Temporal Logics Over Finite Traces with Uncertainty (Technical Report)

In this paper, we introduce an alternative approach to Temporal Answer Set
Programming that relies on a variation of Temporal Equilibrium Logic (TEL) for
finite traces. This approach allows us to even out the expressiveness of TEL
over infinite traces with the computational capacity of (incremental) Answer
Set Programming (ASP). Also, we argue that finite traces are more natural when
reasoning about action and change. As a result, our approach is readily
implementable via multi-shot ASP systems and benefits from an extension of
ASP's full-fledged input language with temporal operators. This includes future
as well as past operators whose combination offers a rich temporal modeling
language. For computation, we identify the class of temporal logic programs and
prove that it constitutes a normal form for our approach. Finally, we outline
two implementations, a generic one and an extension of clingo.

介绍了一种基于 Temporal Equilibrium Logic 的替代方法，用于有限 trace 的 Temporal Answer Set Programming，可实现多通 Answer Set Programming 系统，并结合时间运算符扩展输入语言，同时提供了时间建模语言。