The complexity of linear-time temporal logic over the class of ordinals
我们考虑的时间逻辑与因为和直到模态。这种时态逻辑在表达上等价于一阶逻辑的坎普定理。我们证明了它有一个PSPACE-完全可满足性问题的序数类。在我们的证明的后果，我们表明，给定的代码的一些可数序数α和一个公式，我们可以在PSPACE中决定是否有一个模型的α公式。为了证明这些结果，我们引入了一类简单的序数自动机，作为表达Büchi序数自动机。通过将时态逻辑的可满足性问题归结为简单有序自动机的非空性问题，得到了时态逻辑可满足性问题的PSPACE上界。
2010-12-21 cs.LO
Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables
我们证明了分支时间时序逻辑CTL和CTL*，以及交替时间时序逻辑ATL和ATL*，在具有单个命题变量的语言中与在完整语言中一样具有语义表达性，即，有无限的命题变量由此可见，对于CTL和ATL，用单个变量的可满足性是EXPTIME-完全的，而对于CTL* 和ATL*，用单个变量的可满足性是2 EXPTIME-完全的，即，对于这些逻辑，只有一个变量的公式的可满足性与任意公式的可满足性一样困难。
2019-01-18 cs.LO
On complexity of propositional Linear-time Temporal Logic with finitely many variables
众所周知[DemriSchnoebelen 02]，命题线性时间时态逻辑LTL的可满足性和模型检查问题，在语言中只有一个命题变量，都是PSPACE完全的，这与LTL的这些问题的复杂性相一致，具有任意数量的命题变量[SislaClarke 85]。在本文中，我们表明，通过修改[SislaClarke 85]中LTL的空间硬度的原始证明，可以得到相同的结果;即，我们展示了如何修改来自[SislaClarke 85]的构造，以仅使用一个变量的公式来模拟多项式空间约束的图灵机的计算。我们相信，我们对[DemriSchnoebelen 02]结果的替代证明提供了对LTL的语义和计算特性的额外见解。
2018-11-25 cs.LO
Complexity of Safety and coSafety Fragments of Linear Temporal Logic
本文系统分析 LTL 的 safety 与 cosafety 片段在有限和无限轨迹上的可满足性、有效性及可实现性复杂性，揭示可实现性问题的复杂度分层及轨迹有限性带来的差异。
2025-03-12 cs.LO
Identifying Tractable Quantified Temporal Constraints within Ord-Horn
本文研究了时间结构的量化约束满足问题复杂性，为 Ord-Horn 片段提供了 P 或 coNP-hard 的复杂性二分法，并解决了悬置十多年的 $(\mathbb{Q};x=y\Rightarrow x\geq z)$ 问题复杂性。
2024-02-14 cs.LO
Metric Temporal Extensions of DL-Lite and Interval-Rigid Names
DL-Lite描述逻辑允许在数据库之上对领域知识进行建模，并进行高效推理。我们重点研究了DL-Lite_bool及其片段的度量时态扩展，并研究了可满足性的复杂性。特别是，我们调查的影响，刚性和区间刚性的符号，这使得建模知识，仍然有效的（一段时间）。我们表明，特别是后者增加了相当大的表达能力，在许多逻辑，但它们并不总是增加复杂性。
2018-08-06 cs.LO
Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
从计算复杂性的角度研究了分支时间逻辑CTL的可满足性问题。严格的上限和下限提供了每个时间操作符片段。在平行，最小模型的大小进行了研究，一个合适的概念极小。第三，研究了平坦的CTL，即，时态运算符嵌套深度非常低的公式。在复杂性和最小模型方面显示出尖锐的二分法：时间深度1具有低表达能力，而时间深度2相当于完整的CTL。
2017-02-24 cs.CC cs.LO
Computational Complexity of Standpoint LTL
本文分析立场线性时态逻辑SLTL的计算复杂度，证明其可满足性问题为EXPSPACE完全，还提出约束方法得到PSPACE完全的SLTL片段，实现立场逻辑与LTL的低复杂度结合。
2024-08-16 cs.LO
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
度量时态逻辑$\mtlfull$是研究最多的实时逻辑之一。它表现出相当大的多样性的表达性和可判定性的基础上允许的一套模式和时间间隔的限制$I$的性质。\oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.}在本文中，我们通过证明$\mtlsns$（其中$NS$表示非奇异区间）的可满足性在有限逐点严格单调时间上也是可判定的，从而加强了可判定性结果。我们利用时间投影技术给出了从Ouaknine和Worrell的逻辑$\mtls…
2013-11-27 cs.LO
The Complexity of Learning Linear Temporal Formulas from Examples
CNRS（法国国家科学研究中心）；LaBRI（波尔多计算机科学实验室）；Université de Bordeaux（波尔多大学）；The Alan Turing Institute（艾伦·图灵研究所）
本文研究了从实例中学习线性时态逻辑公式的计算复杂性。我们构造LTL片段的近似算法，并证明了硬度结果，特别是我们得到紧界近似的片段只包含下一个操作符和连接，并证明NP-完全性结果的许多片段。
2021-02-01 cs.FL cs.LG cs.LO
Data Complexity and Rewritability of Ontology-Mediated Queries in Metric Temporal Logic under the Event-Based Semantics (Full Version)
Birkbeck, University of London（伦敦大学伯贝克学院）；University of Oxford（牛津大学）；University of Warsaw（华沙大学）
我们调查的数据复杂性的基于事件的语义下，假设数据实例是有限时间的字时间戳与二进制分数的度量时态逻辑本体介导的回答查询。我们确定类的本体介导的查询回答，可以在AC0，NC1，L，NL，P，和coNP的数据复杂性，提供他们的重写一阶逻辑及其扩展与原始递归，传递闭包或databases，并建立较低的复杂性界限。
2019-07-01 cs.AI cs.CC cs.LO
Interval Temporal Logics over Strongly Discrete Linear Orders: the Complete Picture
区间时态逻辑为线性序域上区间结构的时态推理提供了一个通用的框架，其中区间被视为原始的本体实体。在本文中，我们确定了Halpern和Shoham的区间时序逻辑HS的所有片段的可判定满足性问题的类强离散线性订单。我们根据它们的相对表达能力和复杂性对它们进行分类。我们发现，有44个不同的可判定片段，其复杂性范围从NP到EXPSPACE。此外，我们确定了一些新的不可判定的片段（所有剩余的HS片段已经知道是不可判定的强离散线性订单）。我们通过分析自然数的具体情况来结束本文，自然数的行为与整个强离散线性序类的行为略有不同。在自然数上的可判定片段的数量增加到47：三个不可判定的片段以非原始递归复杂度变得可判定。
2012-10-09 cs.LO
Querying Log Data with Metric Temporal Logic (Technical Report)
我们提出了一个新的框架，基于本体的访问时态日志数据使用的度量时态逻辑MTL的霍恩片段的数据库扩展datalogMTL。我们表明，datalogMTL是ExpSpace完整的，即使与准时的间隔，在这种情况下，充分MTL是已知的不可判定的。我们还证明了非递归datalogMTL是PSpace完全的组合复杂度和AC0的数据复杂度。我们证明了两个现实世界的用例，非递归datalogMTL程序可以表达复杂的时态概念，从典型的用户查询，从而方便访问时态日志数据。我们的实验与西门子涡轮机数据和MesoWest天气数据表明，datalogMTL本体介导的查询是有效的，规模大的数据集。
2018-08-16 cs.LO
Optimal Tableaux Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-time Temporal Logic ATL+
我们开发了一个健全的，完整的，实际上可实现的基于表格的决策方法建设性的可满足性测试和模型合成的片段ATL+的完整交替时间时序逻辑ATL*。该方法扩展了一个基本的方式以前开发的基于表格的ATL的决策方法和工程在2EXPTIME，这是最佳的最坏情况下的可满足性问题的ATL+的复杂性。我们还讨论了如何适当的参数化和语法限制输入ATL+公式类可以降低可满足性问题的复杂性。
2015-05-27 cs.LO
The Complexity of Counting Models of Linear-time Temporal Logic
我们确定的复杂性计数模型的有界大小的规格表示的线性时间时序逻辑。如果边界是以一元形式给出的，那么计算单词模型是P-完全的;如果边界是以二进制形式给出的，那么计算非确定性多项式空间图灵机的运行次数是一样困难的。如果边界是以一元形式给出的，那么对树模型进行计数就像对非确定性指数时间图灵机的接受运行进行计数一样困难。对于边界的二进制编码，这个问题至少和计算非确定性指数空间图灵机的接受次数一样困难。另一方面，它并不比计数非确定性双指数时间图灵机的接受运行更难。
2014-10-06 cs.CC cs.LO
The Complexity of Clausal Fragments of LTL
本文介绍并研究了在时间流（Z，<）上的一些命题时态逻辑LTL的片段。片段的定义，在可用的时间运营商和结构的小句范式的时间公式。我们确定每个片段的可满足性问题的计算复杂性，其范围从NLogSpace到PTime、NP和PSpace。
2013-10-10 cs.CC cs.LO
On the decidability and complexity of Metric Temporal Logic over finite words
度量时态逻辑（Metric Temporal Logic，MTL）是一种重要的实时系统规格说明形式。本文证明了有限时间词上MTL的可满足性问题是可判定的，具有非本原递归复杂性。我们还考虑了MTL的模型检查问题：是否所有的话接受一个给定的Alur-Dill时间自动机满足给定的MTL公式。我们证明了这个问题是可判定的有限字。在无限的话，我们表明，模型检验的安全片段的MTL-其中包括不变性和时间有界的响应特性-也是可判定的。这些结果是相当令人惊讶的，因为它们与文献中出现的各种相反的说法相矛盾。
2007-02-28 cs.CC cs.LO
On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions
本文研究了Halpern和Shoham的区间时序逻辑HS的模型检验问题。在过去的几年里，间隔时态逻辑MC作为传统（基于点）时态逻辑MC的可行替代方案越来越受到关注，传统时态逻辑MC可以被恢复为特殊情况。大多数结果都是在同质性假设下得到的，即约束一个命题字母在一个区间上成立当且仅当它在每个分量状态上成立。最近，Lomuscio和Michaliszyn提出了一种放松这种假设的方法，利用正则表达式来定义命题字母在其组成状态方面的行为。当同质性假设，MC的确切复杂性是一个困难的公开问题，充分HS和它的两个句法最大片段AA'BB' E '和AA' EB 'E'。在本文中，我们提供了一个渐近最优的约束下，这两个片段的复杂性更有表现力的语义变体的基础上，正则表达式的MC问题是AEXP_pol-完成，其中AEXP_pol表示的复杂性类的问题，由指数时间有界的交替图灵机，使一个多项式有界的交替。
2017-09-07 cs.CC cs.LO
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
研究了具有团队语义的模型检验线性时态逻辑（TeamLTL）的表达性和复杂性。TeamLTL，尽管是一个纯粹的模态逻辑，但能够定义超属性，即，与多个执行跟踪相关的属性。TeamLTL最近才被引入，关于它的表达能力和模型检验问题，只有很少的结果是已知的。我们将TeamLTL的表达性与通过用迹和命题量词（HyperLTL和HyperQPTL）扩展LTL获得的超性质的逻辑联系起来。通过这样做，我们得到了一些模型检验的TeamLTL结果，并确定其不可判定性边界。特别是，我们证明了任何向下封闭的TeamLTL扩展的所谓的左平坦片段的模型检验的可判定性。此外，我们建立了具有布尔析取和包含原子的TeamLTL的模型检验问题是不可判定的。
2021-11-23 cs.CC cs.LO
Temporal Conjunctive Query Answering in the Extended DL-Lite Family
基于本体的查询应答（OBQA）通过将领域知识编码在本体中来增强数据库中的经典查询应答。OBQA系统使用本体知识来推断数据中未明确给出的新信息。此外，他们通常采用开放世界假设，这意味着数据中没有明确说明的知识以及没有推断的知识不会被假设为真或假。然而，经典的OBQA只考虑数据的快照，这意味着关于数据的时间演化的信息不用于推理，因此丢失了。我们调查时间合取查询（TCQs），允许通过经典本体访问时态数据。特别是，我们研究了结合和数据复杂性的TCQ蕴涵的本体描述逻辑从扩展的DL-Lite家庭。这些逻辑中的许多允许有效的推理在非时态设置，并成功地应用于实践。我们展示了这些逻辑的时间推理的综合复杂性结果。
2020-03-20 cs.LO
Bounded Variability of Metric Temporal Logic
以前的工作表明，推理与实时时序逻辑往往是简单的限制模型与有界的变化-其中不超过v事件可能会发生每V个时间单位，对于给定的v，V.推理公式与内在的有界的变化，可以采用更简单的技术，依赖于有界的变化，而不损失任何的一般性。那么，在算法上决定哪些公式具有内在的有限可变性的复杂性是什么呢？在本文中，我们研究的问题，参照度量时态逻辑（MTL）。我们证明了在稠密时间模型上，MTL公式的有界可变性是不可判定的，但其不可判定度低于一般稠密时间MTL可满足性。相反，在离散时间模型上，确定MTL有界可变性具有与可满足性相同的指数空间复杂度。为了补充这些负面的结果，我们还简要地讨论了小片段的MTL，更适合推理有界变异。
2014-07-04 cs.LO
Complexity of Timeline-Based Planning over Dense Temporal Domains: Exploring the Middle Ground
在本文中，我们解决的复杂性问题，基于时间线的规划密集的时间域。规划问题是通过一组独立的，但相互作用，组件，每个组件表示的一些状态变量，其行为随时间（时间轴）是由一组时间约束（同步规则）。虽然时间域通常被假设为离散的，但在这里我们考虑密集的情况。密集的时间线为基础的规划最近已被证明是不可判定的一般情况下，可判定性（NP-完全性）可以恢复限制到纯粹的存在同步规则（无规则）。在本文中，我们探讨了这两个极端之间的中间情况下未探索的领域。我们首先表明，可判定性和非原始递归硬度可以证明，通过承认同步规则与触发器，但迫使他们适当地检查约束，只有在未来的触发器（未来的简单规则）。通过在未来的简单规则中额外地约束区间的形式，可以获得更“易处理”的结果：通过避免奇异区间来保证EXPSPACE完备性，通过只允许[0，a]和[b，$\infty$ [..
2018-09-10 cs.CC cs.LO
Strong Backdoors for Linear Temporal Logic
本文针对Fisher提出的线性时态逻辑的CNF-片断，将强后门的概念引入时态逻辑领域。我们研究了以后门大小为参数的可满足性问题的参数化复杂性。我们将后门检测和后门评估区分为horn和krom公式的片段。在这里，我们对全局操作符的操作符片段进行分类，用于过去或未来，以及两者的组合。检测被证明是在FPT，而评价的复杂性表现不同。我们表明，克罗姆公式的问题是paraNP-完全的。对于喇叭公式的复杂性被证明是固定参数易处理或paraNP-完全取决于所考虑的运营商片段。
2016-02-16 cs.CC cs.LO
Generalizing Non-Punctuality for Timed Temporal Logic with Freeze Quantifiers
度量时态逻辑（MTL）和时间命题时态逻辑（TPTL）是线性时态逻辑（LTL）的重要实时扩展。在一般情况下，这些扩展的可满足性检查问题是不可判定的，当未来的U和过去的S模态使用。在一个经典的结果中，证明了MTL [U，S]的非准时片段MITL[U，S]的可满足性检验是可判定的，具有EXPSPACE完全复杂性。鉴于这种非准时性的概念在TPTL[U，S]的情况下不能恢复可判定性，我们提出了TPTL[U，S]的非准时性的一个推广，称为\emph{non adjacency}，并专注于它的1-变量片段1-TPTL[U，S].虽然非相邻的1-TPTL[U，S]似乎是一个非常小的片段，但它比MITL更严格地表达。作为我们的主要结果，我们证明了非相邻1-TPTL[U，S]的可满足性检验问题是可判定的，具有EXPSPACE完全复杂性。
2021-09-05 cs.LO
Tractability Frontier for Dually-Closed Temporal Quantified Constraint Satisfaction Problems
时态（约束）语言是一种关系结构，其一阶定义为有理数，其阶数为。我们在这里研究的时间约束语言的量化约束满足问题（QCSP）的复杂性。我们的主要贡献是一个二分法的限制类双封闭的时间语言。我们证明了这样一种语言的QCSP要么在多项式时间内是可解的，要么对于NP或coNP是困难的。我们的结果推广了类似的二分法QCSP的平等语言，这是关系结构定义的布尔组合的等式。
2021-09-06 cs.LO
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
各种时间属性验证技术将时间验证转换为安全验证。对于无限状态系统，这些变换本质上是不精确的。也就是说，在某些情况下，时间属性成立，但所得到的安全属性不成立。本文介绍了一种解决这种不精确性的机制。这种机制，我们称之为时间预言，是受到预言变量的启发。时间预言通过一个合适的tableau结构，使用一阶线性时间逻辑公式来细化一个无限状态系统。对于一个特定的基于一阶逻辑的liveness-to-safety转换，我们证明了严格使用时间预言可以提高精度。此外，时间预言导致的证明方法的鲁棒性，这是由削减消除定理。我们将我们的方法集成到常春藤演绎验证系统，并表明它可以处理具有挑战性的时间验证的例子。
2021-06-02 cs.LO
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-16 cs.FL cs.LO
First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries
针对基于本体的时态数据访问问题，将扩展的DL-Lite逻辑与离散时间（Z，<）上的线性时态逻辑LTL相结合，设计了二维的【形】时态本体和查询语言.我们主要关注的是一阶重写的本体介导的查询（OMQs），包括一个二维本体和一个积极的时间实例查询。我们的FO重写的目标语言是两个排序的FO（<）-一阶逻辑，其对时刻的排序由内置的优先关系<排序，而对个体的域-其扩展FOE，其标准同余谓词t \equiv 0 mod n，对于任何固定的n > 1，以及允许关系原语递归的FO（RPR）。在电路复杂性方面，FOE和FO（RPR）可重写性分别保证在统一AC 0和NC 1中回答OMQ。我们分三步进行。首先，我们定义了一个层次结构的二维DL-Lite/LTL本体语言和原子查询的OMQ的FO-重写性，通过构建到一维LTL OMQ的投影，并采用最近的结果对命题LTL OMQ的FO-重写性。由于预测涉及确定本体和数据的一致性，我们也考虑了我们的语言的一致性问题。虽然不确定性的一致性与表达布尔角色夹杂物的2D本体语言可能是预期的，我们还表明，而令人惊讶的是，限制克罗姆和霍恩的角色夹杂物导致可判定性（和ExpSpace完整性），即使一个承认完整的布尔概念。作为最后一步，我们解除原子OMQ的可重写性结果的OMQ与表达积极的时态实例查询。提升结果是基于对规范模型的深入研究，并且只涉及Horn本体。
2022-10-21 cs.DB cs.LO
Unifying Hyper and Epistemic Temporal Logic
在文献中，已经提出了两个强大的时序逻辑形式主义表达信息流的安全性要求，在一般情况下，超越常规的属性。一个是经典的，基于认知逻辑的知识模态。另一个，所谓的超逻辑，是最近的，包括许多建议，从文献中，它是基于明确的和同时量化多个路径。为了更好地理解这些逻辑如何相互比较，我们考虑了逻辑KCTL*（CTL* 的知识模态和同步完美回忆语义的扩展）和HyperCTL*。我们首先确定KCTL* 和HyperCTL* 在表达上是不可比的。其次，我们引入并研究了HyperCTL* 的自然线性过去扩展，以统一KCTL* 和HyperCTL*;事实上，我们表明KCTL* 可以很容易地在线性时间内转换为所提出的逻辑。此外，我们证明了这种新的逻辑的模型检测问题是可判定的，我们提供了它的确切的计算复杂性方面的一个新的措施的路径量词的交替。为此，我们解决了开放的复杂性问题，无限制的量化命题时序逻辑。
2014-09-09 cs.LO
Path Checking for MTL and TPTL over Data Words
本文研究了数据词上MTL与TPTL的路径检查问题，依据寄存器数量和约束编码方式给出完整复杂度分析，证明MTL为P完全、TPTL为PSPACE完全，并得出单计数器机器模型检查的精确复杂度。
2017-09-01 cs.LO
MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties
我们提出了月光，用于监测移动和空间分布的网络物理系统（CPS）的时间和时空属性的工具。在所提出的框架中，空间被表示为一个加权图，描述的拓扑配置中的单个CPS实体（图的节点）的安排。节点和边都具有建模物理和逻辑量的属性，这些物理和逻辑量可以随时间变化。MoonLight是用Java实现的，支持时空到达和逃逸逻辑（STREL）的监控。MoonLight可以作为一个独立的命令行工具，作为一个Java API，或通过Matlab接口。我们在这里提供了一些例子，使用Matlab接口，我们评估的工具性能也通过与其他专门用于监测时间属性的工具进行比较。
2021-04-29 cs.LO
Robust Probabilistic Temporal Logics
本文对概率系统的核心规范语言 PCTL 与 PCTL* 进行鲁棒化扩展，并证明相应模型检测问题的复杂度保持不变。
2024-08-05 cs.FL cs.LO
Alternating-time temporal logic with finite-memory strategies
不完全信息的交替时序逻辑ATL和ATL* 的模型检查对于完美召回语义是不可判定的。然而，当限制到无记忆策略的模型检查问题变得可判定。在本文中，我们考虑其他两种类型的语义有限记忆策略的基础上。一种是允许的内存大小有界，另一种是内存大小无界（但必须是有限的）。这是由具有完美召回语义的模型检查的高复杂性和无记忆策略的严重限制所激发的。我们表明，这两种类型的语义介绍是不同的完美召回和无记忆语义和下一个重点的可判定性和复杂性的模型检查在完整和不完整的信息游戏ATL/ATL*。特别是，我们证明了模型检测的复杂性与有界记忆语义是Delta_2 p-完全的ATL和PSPACE-完全的ATL* 在不完全信息的游戏，就像在无记忆的情况下。我们还提出了一个证明，ATL和ATL* 模型检查是不可判定的n >= 3的球员与有限记忆语义的不完全信息游戏。
2013-07-17 cs.GT cs.LO
A Cookbook for Temporal Conceptual Data Modelling with Description Logics
Free University of Bozen-Bolzano（博尔扎诺自由大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
我们设计了适用于时态概念数据模型推理的时态描述逻辑，并研究了它们的计算复杂性。我们的形式主义是基于DL-Lite逻辑与三种类型的概念包含（范围从原子概念包含和不相交的完整布尔），以及基数约束和角色包含。在时间维度上，它们捕获未来和过去的时间操作符的概念，灵活和刚性的角色，操作符的“总是”和“一些时间”的角色，数据断言的特定时刻的时间和全球概念的包容性。这些逻辑被解释为对象域和时间流（Z，<）的笛卡尔积，满足恒定域假设。我们证明，我们的时间描述逻辑（它可以捕捉生命周期基数和定性或定量的进化约束）最具表现力的结果是不可判定的。然而，通过省略概念/角色上的一些时态运算符或通过限制概念包含的形式，我们获得了复杂度介于PSpace和NLogSpace之间的逻辑。这些积极的结果是通过减少到命题时态逻辑的各种子句片段，这开辟了一条道路，采用命题或一阶时态证明推理的时间数据模型。
2014-05-02 cs.AI cs.LO
On the Complexity of Realizability for Safety LTL and Related Subfragments
我们研究了安全LTL的可实现性问题，安全LTL是线性时态逻辑的语法片段，用于捕获安全公式。我们证明了该问题是EXP-完全的，反驳了现有的2 EXP-完全性猜想。我们通过比较安全LTL与看似较弱的亚片段的复杂性来实现这一点。特别是，我们表明，安全LTL的每一个公式可以减少到一个等价实现的公式的形式$α\land \Box ψ$，其中$α$是一个目前的公式系统变量和$ψ$包含下作为唯一的时间运营商。这个新片段的可实现性问题，我们称之为$\mathsf{GX}_{\mathsf{0}}$，也是EXP完全的。
2022-01-19 cs.CC cs.LO
Deterministic Temporal Logics and Interval Constraints
在时态逻辑中，一个中心问题是关于模态的选择及其相对表达能力，与决策问题的复杂性（如可满足性）相比。在本教程中，我们将说明在有限字模型上对此类问题的研究，首先是Schutzenberger最初定义的Unambient Starfree正则语言（UL）的逻辑，然后是带约束的扩展，它出现在区间逻辑中。我们提出了确定性的时间逻辑，与不同的方式，这也表征UL。所使用的工具和技术以“海龟程序”或“排名”的名义进行。这些都是简单的自动机。我们使用的性质，如秩方向性和秩凸性，以显示所有这些逻辑具有NP可满足性。其中一些模态的递归扩展使我们能够在有限线性阶上充分利用一阶逻辑。我们还讨论了区间约束模态扩展确定性时序逻辑，中间的表达。这些允许计数或简单的代数运算的路径。这些扩展逻辑的复杂度是PSpace，就像全时态逻辑一样（当使用二进制表示法时是ExpSpace）。
2017-03-07 cs.FL cs.LO
Verifying linear temporal specifications of constant-rate multi-mode systems
本文提出面向恒速率多模式系统的 LTL 变体，并刻画其句法子片段的模型检验复杂度，得到 P 完全、NP 完全或不可判定的统一分类。
2023-04-26 cs.CC cs.FL cs.LO
Temporal Logic for Social Networks
本文介绍了一种基于标准线性时态逻辑（LTL）的具有一类社会网络模型的逻辑，利用现有模型检查器的功能来分析社交网络。我们提供了一个简短的文献综述，然后定义我们的逻辑和公理化，提出了一些简单的动机的例子，模型和公式，并通过翻译成命题公式，显示其合理性和完整性。最后，我们简要讨论了模型检验和时间复杂度分析。
2021-03-12 cs.LO cs.SI
Complexity of ITL model checking: some well-behaved fragments of the interval logic HS
模型检验已成功地应用于许多计算机科学领域，包括人工智能、理论计算机科学和数据库。大多数提出的解决方案利用经典的，基于点的时序逻辑，而很少的工作已经做了区间时序逻辑设置。最近，人们提出了有限Kripke结构上Halpern和Shoham的时间区间HS模态逻辑的非初等模型检验算法（在齐性假设下）和它的两个有意义片段的EXPSPACE模型检验过程.在本文中，我们表明，更有效的模型检验程序可以开发一些表达足够的片段HS。
2016-01-13 cs.CC cs.DS cs.LO
Changing Observations in Epistemic Temporal Logic
ENS Rennes（雷恩高等师范学院）；University of Naples “Federico II”（那不勒斯费德里科二世大学）
我们研究了知识和时间逻辑中主体观察力的动态变化。我们认为CTL*K，扩展CTL* 与知识运营商，并丰富它与一个新的运营商，模拟一个代理的方式观察系统的变化。我们扩展了经典的语义知识的完美召回代理占观察的变化，我们表明，这个新的运营商严格增加了CTL*K的表达能力。我们减少模型检查问题，我们的逻辑CTL*K，这是已知的可判定的。这为我们的逻辑提供了模型检查问题的解决方案，但其复杂性不是最佳的。事实上，我们提供了一个更好的复杂性直接决策过程。
2018-09-03 cs.AI cs.LO cs.MA
The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments
在1985年的一篇开创性论文中，Sistla和Clarke证明了线性时态逻辑（LTL）的模型检验问题是NP完全的或PSPACE完全的，这取决于所使用的时态运算符的集合。相反，如果命题算子的集合是有限的，复杂性可能会降低。本文系统地研究了命题算子和时态算子限制集上LTL公式的模型检验问题。对于几乎所有的时间和命题运算符的组合，我们确定是否模型检验问题是易处理的（在P）或难处理的（NP难）。然后，我们专注于易处理的情况下，表明他们都是NL-完全的，甚至对数空间可解。这导致了一个令人惊讶的差距之间的复杂性和棘手的案件。值得注意的是，我们的分析涵盖了无限的问题集，因为有无限多组命题算子。
2008-05-05 cs.CC cs.LO
The Transformation Logics
University of Oxford（牛津大学）
本文提出一族以变换算子为核心的新型时序逻辑，尤其利用基于半群的算子构建表达能力与复杂度递增的层级，为不同应用的权衡需求提供新框架。
2024-09-06 cs.AI cs.FL cs.LO
A Temporal Logic for Hyperproperties
克拉克森和施奈德引入的超属性将计算机程序的正确性描述为其计算路径集的条件。标准时态逻辑一次只能引用一条路径，因此无法表达许多感兴趣的超性质，包括不干涉和安全和编码理论中的其他重要性质。本文研究了具有显式路径变量的时态逻辑的扩展。我们表明，量化的路径自然包含其他扩展的时间逻辑与运营商的信息流和知识。具有路径量化的时序逻辑的模型检验问题是可判定的。对于交替深度1，复杂度在公式长度上是PSPACE，在系统大小上是NLOGSPACE，就像线性时间时态逻辑一样。
2013-06-27 cs.CR cs.LO
Learning temporal formulas from examples is hard
University of Bordeaux（波尔多大学）；CNRS（法国国家科学研究中心）
本文研究从示例中学习线性时序逻辑公式的计算复杂性，证明该问题对完整逻辑及几乎所有片段均为NP完全，凸显了表达区分属性的难度，并推动高效启发式方法的探索。
2023-12-26 cs.AI cs.FL cs.LG
Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems
Carnegie Mellon University（卡内基梅隆大学）
本文结合量化微分动态逻辑与时序逻辑，提出一种验证分布式混合系统时序与非时序性质的方法，并给出相对完备的模块化验证演算。
2012-07-11 cs.LO cs.SY eess.SY
