arXiv 2102.008762021-02-01cs.FLcs.LGcs.LO

The Complexity of Learning Linear Temporal Formulas from Examples

CNRS（法国国家科学研究中心）；LaBRI（波尔多计算机科学实验室）；Université de Bordeaux（波尔多大学）；The Alan Turing Institute（艾伦·图灵研究所）

Nathanaël Fijalkow, Guillaume Lagarde

英文摘要：

In this paper we initiate the study of the computational complexity of learning linear temporal logic (LTL) formulas from examples. We construct approximation algorithms for fragments of LTL and prove hardness results; in particular we obtain tight bounds for approximation of the fragment containing only the next operator and conjunctions, and prove NP-completeness results for many fragments.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

带过去时态的无主体交替认知度量时态逻辑：模型检查与复杂性

Agent-Alternation-Free Epistemic Metric Temporal Logic with Past: Model Checking and Complexity

Université Paris-Saclay（巴黎萨克雷大学）；CNRS（法国国家科学研究中心）；ENS Paris-Saclay（巴黎萨克雷高等师范学校）；LMF（拉格兰日数学实验室）；Institut Universitaire de France（法兰西学院）；Direction Générale de l’Armement（法国国防总局）

研究带过去时态的无主体交替认知度量时态逻辑的模型检查，通过结合时态测试自动机与完美回忆观察者进行分析，证明其模型检查为EXPSPACE完全，给出了该逻辑在特定条件下的复杂性结论。

2026-07-16cs.FLcs.LO

Learning Temporal Logic Properties: an Overview of Two Recent Methods

Carl von Ossietzky University of Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）

Learning linear temporal logic (LTL) formulas from examples labeled as positive or negative has found applications in inferring descriptions of system behavior. We summarize two methods to learn LTL formulas from examples in two different problem settings. The first method assumes noise in the labeling of the examples. For that, they define the problem of inferring an LTL formula that must be consistent with most but not all of the examples. The second method considers the other problem of inferring meaningful LTL formulas in the case where only positive examples are given. Hence, the first me…

2022-12-02cs.AIcs.FLcs.LG

从示例中学习时序公式是困难的

Learning temporal formulas from examples is hard

University of Bordeaux（波尔多大学）；CNRS（法国国家科学研究中心）

本文研究从示例中学习线性时序逻辑公式的计算复杂性，证明该问题对完整逻辑及几乎所有片段均为NP完全，凸显了表达区分属性的难度，并推动高效启发式方法的探索。

2023-12-26cs.AIcs.FLcs.LG

验证恒速率多模式系统的线性时序规约

Verifying linear temporal specifications of constant-rate multi-mode systems

本文提出面向恒速率多模式系统的 LTL 变体，并刻画其句法子片段的模型检验复杂度，得到 P 完全、NP 完全或不可判定的统一分类。

2023-04-26cs.CCcs.FLcs.LO

Deterministic Temporal Logics and Interval Constraints

In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiability. In this tutorial, we will illustrate the study of such questions over finite word models, first with logics for Unambiguous Starfree Regular Languages (UL), originally defined by Schutzenberger, and then for extensions with constraints, which appear in interval logics. We present Deterministic temporal logics, with diverse sets of modalities, which also characterize UL. The tools and techniques used go under t…

2017-03-07cs.FLcs.LO

A Tableau Construction for Finite Linear-Time Temporal Logic

This paper describes a method for converting formulas in finite propositional linear-time temporal logic (Finite LTL) into finite-state automata whose languages are the models of the given formula. Finite LTL differs from traditional LTL in that formulas are interpreted with respect to finite, rather than infinite, sequences of states; this fact means that traditional finite-state automata, rather than ω-automata such as those developed by Büchi and others, suffice for recognizing models of such formulas. The approach considered is based on well-known tableau-construction techniques developed …

2020-06-22cs.FLcs.LO

更多相关论文收起更多论文

Temporal-Logic Query Checking over Finite Data Streams

This paper describes a technique for inferring temporal-logic properties for sets of finite data streams. Such data streams arise in many domains, including server logs, program testing, and financial and marketing data; temporal-logic formulas that are satisfied by all data streams in a set can provide insight into the underlying dynamics of the system generating these streams. Our approach makes use of so-called Linear Temporal Logic (LTL) queries, which are LTL formulas containing a missing subformula and interpreted over finite data streams. Solving such a query involves computing a subfor…

2020-06-06cs.FLcs.LO

变换逻辑

The Transformation Logics

University of Oxford（牛津大学）

本文提出一族以变换算子为核心的新型时序逻辑，尤其利用基于半群的算子构建表达能力与复杂度递增的层级，为不同应用的权衡需求提供新框架。

2024-09-06cs.AIcs.FLcs.LO

Learning Finite Linear Temporal Logic Specifications with a Specialized Neural Operator

Brown University（布朗大学）；UC Berkeley（加州大学伯克利分校）

Finite linear temporal logic ($\mathsf{LTL}_f$) is a powerful formal representation for modeling temporal sequences. We address the problem of learning a compact $\mathsf{LTL}_f$ formula from labeled traces of system behavior. We propose a novel neural network operator and evaluate the resulting architecture, Neural$\mathsf{LTL}_f$. Our approach includes a specialized recurrent filter, designed to subsume $\mathsf{LTL}_f$ temporal operators, to learn a highly accurate classifier for traces. Then, it discretizes the activations and extracts the truth table represented by the learned weights. Th…

2021-11-21cs.AIcs.FL