A Survey on Temporal Logics
Savas Konur
本文综述了广义时态逻辑的主要研究和最新研究，介绍了各种时态逻辑系统，处理了各种时态结构，讨论了时态逻辑的重要特征，如可判定性（或不可判定性）结果、可表达性和证明系统。
This paper surveys main and recent studies on temporal logics in a broad sense by presenting various logic systems, dealing with various time structures, and discussing important features, such as decidability (or undecidability) results, expressiveness and proof systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
本文综述了近年来通过符号模型检验验证时态认知逻辑的一些工作，重点介绍了基于OBDD和基于SAT的离散和实时分支时态逻辑的认知逻辑验证方法。
Logic Column 11: The Finite and the Infinite in Temporal Logic
本文研究了有限和无限序列上的LTL时态算子的解释。这是用来作为一个健全的和完整的公理化的Caret，最近的时间逻辑推理嵌套过程调用和返回的程序推导的基础。
Interval Temporal Logic Decision Tree Learning
决策树是一种简单但功能强大的分类模型，用于分类分类和数值数据，尽管简单，但它们通常用于运筹学和管理以及知识挖掘。从逻辑的角度来看，决策树可以看作是用命题逻辑编写的逻辑规则的结构化集合。由于知识挖掘正迅速向时态知识挖掘发展，并且由于在许多情况下时态信息最好由区间时态逻辑描述，因此命题逻辑决策树可能向区间时态逻辑决策树发展。本文定义了区间时态逻辑决策树学习问题，并提出了一种推广经典决策树学习的解决方案。
Erratum to "Frequency Linear-time Temporal Logic"
我们修正了一个定理的证明，该定理表明频率线性时间时序逻辑的可满足性是不可判定的[TASE 2012]。
$ω$-Forest Algebras and Temporal Logics
我们使用[4]中介绍的无限树语言的代数框架来导出各种时态逻辑的有效特征，特别是逻辑EF（CTL的一个片段）及其计数变体cEF。
Complete Intuitionistic Temporal Logics in Topological Dynamics
线性时态逻辑的语言可以在动态拓扑系统类上解释，从而产生了直观时态逻辑${{\sf ITL}^{\sf c}}_{\Diamond,\forall}$，最近Fernán-Duque证明了它是可判定的。在这篇文章中，我们公理化这个逻辑，一些片段，并证明几个熟悉的空间的完备性。
Systematic Construction of Temporal Logics for Dynamical Systems via Coalgebra
时态逻辑是动态系统的一种明显的高级描述性伴随形式主义，动态系统将行为建模为状态随时间的确定性演化。各种各样的不同的时间逻辑适用于动力系统存在，每个候选人都有自己的实用理由。在这里，提出了一种系统地构建动力系统时态逻辑的方法：首先，注意到动力系统可以以多种方式被视为余代数。其次，一个简单的标准结构的模态逻辑的余代数，即莫斯的余代数逻辑，应用。最后，所得到的系统的特点是相对于他们表达的时间属性。
Real-time and Probabilistic Temporal Logics: An Overview
在过去的二十年里，人们对用于描述和验证实时的【形】系统的逻辑形式进行了广泛的研究。时态逻辑一直是这一方向的重要研究课题。虽然许多逻辑已经被引入到实时的【形】和复杂系统的形式化规范，这些逻辑的最新全面的分析并不存在于文献中。在本文中，我们分析实时的【形】和概率时态逻辑已被广泛应用于这一领域。我们外推的概念，可判定性，公理化，表达性，模型检验等，为每个逻辑分析。我们还提供了一个比较的时间逻辑讨论的功能。
A Gödel Calculus for Linear Temporal Logic
我们考虑哥德尔时序逻辑（$\sf GTL$），一个变种的线性时序逻辑的基础上哥德尔-达米特命题逻辑。在最近的工作中，我们已经表明，这种逻辑享受自然语义作为一个模糊逻辑和作为一个超直觉逻辑。使用语义学方法，证明了该逻辑是{ \sc pspace}-完全的。在本文中，我们提供了一个演绎演算$\sf GTL$，并表明这种演算是健全的和完整的上述语义。
Linear Temporal Justification Logics with Past Operators
本研究将Artemov证明逻辑与含过去、未来算子的线性时序逻辑结合，构建多种时序证立逻辑并证明其可靠性与完备性，还探究了证立与时间的交互原理。
A Probabilistic Variant of Projection Temporal Logic
在本文中，我们提出了概率离散时间投影时序逻辑（PrPTL），它扩展了投影时序逻辑（PTL）的概率。为此，导出了一些有用的公式，并给出了一些逻辑规律。进一步，我们定义了PrPTL的时间范式（TNF）作为标准形式，并证明了任何PrPTL公式都可以改写为TNF.根据时间范式，构造了时间范式图，并将其用于PrPTL的概率模型检验。
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
有限迹上的时态逻辑与潜在无限迹上的时态逻辑不同。Rozelu首先证明了有限迹上线性时态逻辑（LTLf）的完备性，并提出了一个新的共归纳公理。我们提供了一个不同的证明，用更少，更传统的公理。我们的证明是Kröger和Merz的Henkin-Hasenjaeger式证明的直接改编。我们修改的本质是我们“注入”有限性：也就是说，我们改变证明结构以确保模型是有限的。我们的目标是提出一个全面的，可访问的证据。
Timed context-free temporal logics (extended version)
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（ECNTL）和嵌套度量时序逻辑（NMTL）。ECNTL逻辑是CARET逻辑（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。我们证明了ECNTL的可满足性和可视下推时间自动机VPTA对ECNTL的可视模型检验是可判定的和EXPTIME完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于ECNTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
Characterizing perfect recall using next-step temporal operators in S5 and sub-S5 Epistemic Temporal Logic
我们回顾了解释系统，博弈论和认知逻辑的文献中的完美回忆的概念。在认知时态逻辑（ETL）的背景下，我们给了（据我们所知）一个新的框架条件完美的回忆，这是本地的，可以直接翻译成一个定义公式的语言，只有下一步的时间运营商。这个框架条件也产生了一个完整的公理化的S5 ETL框架与完美的召回。然后，我们考虑如何扩展和巩固的概念，完美的回忆在sub-S5设置，讨论的各种概念不再是等同的。
A Note on Parameterised Knowledge Operations in Temporal Logic
我们认为建模的知识概念的时间逻辑。知识逻辑运算的研究起源于1962年左右，是用模态表示知识和信念。今天，它是一个非常好的地区。然而，我们想从另一个角度来看待它，我们的论文用{ \em past}在线性时态逻辑方面对知识进行建模。我们考虑各种版本的逻辑知识操作，可以在这个框架中定义。技术上，语义，语言和时态知识逻辑的基础上，我们的方法构建。提出了判定算法，并对这种方法的统一性进行了评述。本文不提供强大的新技术输出，而是我们提出了新的方法来概念的知识（在时间方面）。
Reactive Temporal Logic
虽然标准的处理时间逻辑是足够的封闭系统，没有运行时与他们的环境相互作用，他们没有反应系统，通过同步的动作与他们的环境进行交互。本文介绍了反应时态逻辑，一种适用于反应系统研究的时态逻辑形式。我说明了它的使用，应用它来制定一个公平的调度定义，和一个正确的互斥协议。这些概念之前的定义在概念上更加复杂或不太精确，导致了关于给定协议是否满足隐含要求的争论。
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
A survey of computability logic
本文介绍了可计算性逻辑的概况：它的哲学和动机，主要概念和迄今为止取得的最重要的成果。这篇文章的持续更新的在线版本在http://www.csc.villanova.edu/~japaridz/CL/上维护。
Timed Context-Free Temporal Logics
本文的重点是时间逻辑的实时下推反应系统的行为的描述。本文旨在通过确保组合设置中的可判定性和易处理性，来桥接专门用于分别表达密集实时实时属性和上下文无关属性的易处理逻辑。为此，我们引入两个实时线性时序逻辑指定定量定时上下文无关的要求在逐点语义设置：事件时钟嵌套时序逻辑（EC_NTL）和嵌套度量时序逻辑（NMTL）。逻辑EC_NTL是逻辑CaRet（标准LTL的上下文无关扩展）和事件时钟时序逻辑（与事件时钟自动机类相关的易处理实时逻辑框架）的扩展。本文证明了EC_NTL的可满足性和可视下推时间自动机（VPTA）对EC_NTL的可视模型检验是可判定的和EXPTIME-完全的。另一个提出的逻辑NMTL是标准度量时态逻辑（MTL）的上下文无关的扩展。众所周知，未来MTL的可满足性在无限时间词上是不可判定的，但在有限时间词上是可判定的。另一方面，我们表明，通过增加未来的MTL与未来的上下文无关的时间运营商，可满足性问题原来是不可判定的有限时间的话。在积极的一面，我们设计了一个有意义的和可判定的片段的逻辑NMTL，这是表示等价于EC_NTL和可满足性和明显的模型检查的VPTA是EXPTIME完成的。
Time and Gödel: Fuzzy temporal reasoning in PSPACE
我们研究一个非经典版本的线性时序逻辑的命题片段是哥德尔-达米特逻辑（这是众所周知的超直觉逻辑和t-范数模糊逻辑）。我们定义的逻辑使用两个自然语义，实值语义和双关系语义，并表明，这些确实定义了一个相同的逻辑。虽然这哥德尔时序逻辑没有任何形式的有限模型属性，这两个语义，我们证明了每一个可证伪公式是可证伪的有限拟模型，这产生的逻辑的可判定性。然后，我们加强这一结果表明，哥德尔时间逻辑是PSPACE完全的。
Temporal Justification Logic
证明逻辑是模态类逻辑，具有记录句法结构中模态的原因或证明的额外能力，称为证明项。证明逻辑可以被看作是模态逻辑的显式对应物。分布式系统中Agent的行为和交互通常使用知识和时间逻辑来建模。在本文中，我们勾勒出一些初步的想法，如何模态知识的知识和时间的逻辑的一部分，可以用一个适当的理由逻辑。
Efficient First-Order Temporal Logic for Infinite-State Systems
在本文中，我们考虑的规范和验证的无限状态系统使用时序逻辑。特别是，我们描述参数化系统使用一个新的品种的一阶时序逻辑，这是足够强大的这种形式的规范和易于处理的实际演绎验证。重要的是，时态语言的强大功能使我们能够描述（和验证）异步系统，通信延迟和更复杂的属性，如活性和公平性。这些方面对于许多其他无限状态验证方法来说似乎很困难。
Intransitive Linear Temporal Logic, Knowledge from Past, Decidability, Admissible Rules
我们的手稿研究线性时间（与UNTIL和NEXT）逻辑的基础上的概念不传递时间。非传递时间特别是，我们展示了如何在这样的框架中表示知识的概念（在这里，我们认为逻辑操作NN和操作UNTIL（实际上，时间整体）是针对过去）。我们研究的基本数学问题是任何逻辑系统的基本问题-可判定性和可判定性w.r.t.可接受的规则首先，我们考虑具有非一致非传递性的逻辑，并描述如何解决这种逻辑的可判定性问题。然后，我们考虑了这种逻辑的一种修改--具有一致不传递性的线性时态逻辑，并解决了推理规则的可容许性问题。在论文的结论部分列举了一系列有待解决的问题。
Temporal Probabilistic Logic Programs: State and Revision
在许多应用中，我们必须处理与事件相关的时间不确定性。时间概率（TP）逻辑程序应该通过提出不确定时刻的概念来支持事件的有效时间不确定性，即具有相关的上下概率分布的时间点（事件的时间窗）的间隔。特别是，我们提出了新的语义，为TP逻辑程序的Dekhtyar和Subrahmanian。我们的语义，可能的世界语义的基础上，是一个概括的可能的世界语义（非时间）概率逻辑编程，我们定义了新的语法PT程序，明确表示在所有原子的时间变量，并显示如何作为可能的世界概率分布的Herbrand解释的标准作用是连贯地扩展到时间概率逻辑编程。
Expressive Completeness of Metric Temporal Logic
度量时态逻辑（Metric Temporal Logic，MTL）是线性时态逻辑的一种推广，其中Until和Since模态用表示度量约束的间隔来注释。Hirshfeld和Rabinovich的一个开创性的结果表明，在实数上，具有二进制顺序关系<和一元函数+1的一阶逻辑严格地比具有整数常数的MTL更具表达性。事实上，他们证明，没有时间逻辑的模态是由公式定义的有界量词深度可以表达完整的FO（<，+1）。在本文中，我们展示了一个令人惊讶的结果：如果我们在一阶逻辑中允许一元函数+q，（q有理数），并相应地允许MTL中的有理数常数，那么这两个逻辑具有相同的表达能力。这给出了第一个推广的坎普定理的表达完整性的LTL FO（<）的定量设置。这个结果的证明涉及Gabbay的分离概念的推广。
A Complete Mental Temporal Logic for Intelligent Agents
该研究提出融合心智模态的时态逻辑 BPICTL，建立可靠完备推理系统、证明有限模型性质并给出模型检测算法。
The logic of temporal domination
针对“A与B几乎同样频繁成立”的公平性条件，论文提出时间支配逻辑，给出语法与语义，并借助 k-counting automata 证明其为线性时间时序逻辑的真正扩展。
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
在本文中，我们提出了一个新的逻辑表示和推理的概率超性质。超性质描述了系统中不同独立执行之间的关系。概率超属性表示这些执行之间的定量依赖关系。概率系统的标准时态逻辑，即，PCTL和PCTL* 一次只能引用一条路径，因此不能表达许多感兴趣的概率超性质。本文提出的逻辑，\HyperPCTL，增加了明确的和同时量化多个跟踪PCTL。这种量化允许表达概率超性质。对于离散时间马尔可夫链，给出了该逻辑的模型检验算法。
Temporalized logics and automata for time granularity
在文献中已经提出了k个后继者的一元二阶理论的适当扩展，以捕获时间粒度的概念。在本文中，我们提供了一元二阶理论的向下无界分层结构，这是无限的可加细的结构，由一个粗域和无限数量的更细和更细的域，和向上无界分层结构，这是由一个最细的域和无限数量的更粗和更粗的域，与表达完全和基本可判定的时间逻辑对应。我们通过两个步骤得到这样的结果。首先，我们定义了一类新的组合自动机，称为时间自动机，它可以被证明是自动机理论对应的时间逻辑，并显示相关的属性，如关闭下的布尔运算，可判定性，并表示等价的时间逻辑，从组件自动机转移到时间的。然后，我们利用时间化逻辑和自动机之间的对应关系，以减少寻找时间粒度理论的时间逻辑对应物的任务，以更容易找到时间化自动机对应物。
Reelay: Online Temporal Logic Monitoring Framework
Reelay 提供了一个统一的在线时序逻辑监控框架，用于对复杂物理系统进行严格分析和运行时验证，支持多种时序逻辑并优化资源使用。
Distributed States Temporal Logic
我们引入了一个时间逻辑的原因在异步设置的全球应用程序。首先，我们定义了分布式状态逻辑（DSL），模态逻辑的地方，嵌入到系统的分布式状态的理论的每个组件的本地理论。我们提供了一个健全的和完整的公理化逻辑。其贡献在于，即使在没有全局时钟的情况下，也可以对涉及多个组件的属性进行推理。然后，我们定义了分布式状态时态逻辑（DSTL），通过引入时态算子的统一。我们支持我们的建议，制定了一对例子：一个简单的安全通信系统，和分布式领导选举的算法。这项工作的动机是，现有的分布式系统的逻辑没有正确的表达能力的原因系统的行为，当通信是基于异步消息传递。另一方面，在对全局应用程序建模时，异步通信是最常用的抽象。
Temporal Logics for Hyperproperties
提出了两种新的超性质验证逻辑。超属性将安全策略（如不干涉）表征为计算路径集的属性。标准的时态逻辑，如LTL、CTL和CTL*，一次只能引用一条路径，因此不能表达许多感兴趣的超性质。这里提出的逻辑，HyperLTL和HyperCTL*，在多个路径上向LTL和CTL* 添加显式和同时量化。这种量化使得能够表达超性质。给出了该逻辑的模型检验算法。针对HyperLTL的一个片段，实现了一个原型模型检测器。
Decidability of the interval temporal logic ABBar over the natural numbers
在本文中，我们把注意力集中在艾伦的关系“满足”，“开始”，“开始于”（简称ABBar），解释了自然数的时间间隔逻辑。我们首先介绍的逻辑，我们表明，它是有足够的表现力来建模独特的区间属性，如完成条件，捕捉基于点的时态逻辑的基本形式，如直到运营商，并编码相关的度量约束。然后，我们证明了ABBar在自然数上的可满足性问题是可判定的，提供了一个小模型定理的基础上原来的压缩方法。最后证明了问题的EXPSPACE-完全性
On the complexity of Temporal Equilibrium Logic
时态平衡逻辑（TEL）是一个很有前途的逻辑框架，它利用LTL风格的时态算子扩展了应答集程序设计的知识表示和推理能力。据我们所知，它是第一个完全适应标准时态逻辑（特别是LTL）的语法而不需要进一步构造的非单调逻辑。本文对TEL公式的时间均衡模型的一致性问题进行了系统的复杂性分析。它以前表明，在一般情况下，这个问题位于PSPACE和EXPSPACE之间的某个地方。在这里，我们建立一个下界匹配已知的EXPSPACE上界。此外，我们分析了各种自然的TEL公式子类的复杂性，确定易处理和难处理的片段。最后，本文通过解决极小LTL模型的可满足性问题，对逻辑LTL提供了一些新的见解。得到的复杂性结果突出了解释LTL有限或无限的话之间的实质性差异。
The complexity of linear-time temporal logic over the class of ordinals
我们考虑的时间逻辑与因为和直到模态。这种时态逻辑在表达上等价于一阶逻辑的坎普定理。我们证明了它有一个PSPACE-完全可满足性问题的序数类。在我们的证明的后果，我们表明，给定的代码的一些可数序数α和一个公式，我们可以在PSPACE中决定是否有一个模型的α公式。为了证明这些结果，我们引入了一类简单的序数自动机，作为表达Büchi序数自动机。通过将时态逻辑的可满足性问题归结为简单有序自动机的非空性问题，得到了时态逻辑可满足性问题的PSPACE上界。
Two-Way Unary Temporal Logic over Trees
我们考虑一个无秩、无序的有限树的时态逻辑EF+F^-1。该逻辑有两个运算符：EF，表示“在某些适当的后代继承中”，F^-1，表示“在某些适当的祖先继承中”。我们提出了一个算法，用于判定一个无秩有限树的正则语言是否可以用EF+F^-1表示。该算法使用的表征表示的森林代数。
Automata-Theoretic Characterisations of Branching-Time Temporal Logics
本文通过识别Hesitant Tree Automata的两个变体，为任意分支树上的CTL*和ECTL*等分支时间时序逻辑提供了自动机理论刻画，解决了悬而未决四十年的开放问题。
The Last Paper on the Halpern-Shoham Interval Temporal Logic
Halpern-Shoham逻辑是时间间隔的模态逻辑。在过去的十年里，人们已经做出了一些努力，根据可满足性问题的可判定性对这个美丽逻辑的片段进行分类。我们有助于这一努力显示-我们认为是一个相当意外的结果-的逻辑的子区间，片段的Halpern-Shoham，其中只有运营商“期间”，或D，是允许的，是不可判定的离散结构。这是令人惊讶的，因为这个逻辑是可判定的密集秩序和其自反的变种是已知的可判定的离散结构。
Temporal Logics on Words with Multiple Data Values
本文提出并研究了属性词的时态逻辑，即在每个位置具有（有限）（属性，值）对集合的数据词。它认为一个基本的逻辑是一个语义片段的逻辑$LTL^\downarrow_1$的Demri和Lazic与运营商导航到未来和过去。通过对数据自动机的空性问题的简化，证明了这种基本逻辑是可判定的。虽然基本逻辑只允许导航到出现固定数据值的位置，但扩展也允许导航到具有不同数据值的位置。除了一些不可判定的结果外，还证明了具有不等式目标条件的UNTIL算子的扩张是可判定的。
On the Complexity of Linear Temporal Logic with Team Semantics
在线性时序逻辑（LTL）中，一个以公式形式给出的规范通过一组迹来定义一个系统。然而，某些功能，如信息流的安全约束，而不是作为所谓的hyperproperties，这是一套套的痕迹。一种逻辑方法是团队逻辑，这是一个逻辑框架，用于规范信息的依赖性和独立性。团队语义的LTL最近被发现是超属性的逻辑。我们研究了具有同步团队语义和布尔否定的LTL的复杂性理论，证明了LTL的模型检验和可满足性问题都是高度不可判定的，等价于三阶算术的判定问题.此外，我们证明，这种复杂性已经出现在小的时间深度和只有“未来”模态F。最后，我们还介绍了口吃不变性的团队语义推广。
First-order Temporal Logic on Finite Traces: Semantic Properties, Decidable Fragments, and Applications
基于有限严格线性顺序的时态逻辑的形式主义，在文献中称为有限迹，已被用于自动规划，过程建模，（运行时）验证和程序合成中的时态规范，以及知识表示和推理。本文主要研究有限迹上的一阶时态逻辑。我们首先调查保存有限和无限的痕迹之间的公式的等价性和可满足性，通过提供一组语义和句法条件，以保证在这两种情况下推理之间的区别可以模糊。此外，我们表明，满足性问题的有限迹几个可判定的片段的一阶时序逻辑是ExpSpace完全的，在无限迹的情况下，而它减少到NExpTime有限迹有界的时刻数被认为是。这也导致了新的复杂性结果的时间描述逻辑在有限的痕迹。最后，我们调查应用程序的规划和验证，特别是通过建立连接的概念不敏感的无限性和安全性的文献。
Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics
本文提出一种Tseitin风格的翻译，将任意度量时序公式映射到仅含过去算子的逻辑程序片段，从而利用回答集编程求解器进行推理。
Molecular Model Checking a Temporal Logic
分子计算已经成功地用于解决越来越多的复杂计算问题。然而，作为一个重要的复杂问题，模型检验在分子计算环境下还远未得到完全解决，因为它仍然缺乏方法。为了解决这个问题，一个模型检验方法提出了一个给定的时序逻辑使用分子计算检查的基本结构。通过设计新的编码和调用这个过程，我们得到了一个基于分子的方法来检查这个逻辑的所有基本结构。
A survey of proof nets and matrices for substructural logics
本文是一个调查的两种“压缩”证明计划，\emph{matrix method}和\emph{proof nets}，适用于各种逻辑沿着子结构层次从经典的所有方式到非关联的Lambek系统。为后者提供了一种新的处理证明网。证明网和矩阵的描述给出了一个统一的符号序列的基础上，使各种逻辑的计划的属性可以很容易地进行比较。
Linear Non-Transitive Temporal Logic, Knowledge Operations, Algorithms for Admissibility
本文研究了非传递时态线性逻辑LTL（Past，m）中推理规则的可满足性、可判定性和可容许性、知识概念和主体知识等问题。我们发现算法解决上述问题，证明我们的方法考虑线性非传递时间与几个例子。主要的、最复杂的、技术上的新结果是LTL（Past，m）w.r.t.可接受的规则我们讨论了几种方法来形式化的知识和代理的知识在给定的方法在非传递线性逻辑模型指向过去的概念。
Robust Alternating-Time Temporal Logic
本文提出扩展自ATL/ATL*的鲁棒交替时间时序逻辑rATL与rATL*，通过多值语义实现多智能体系统鲁棒策略推理，验证其模型检测与可满足性问题未增加计算复杂度。
A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking
概率计算树逻辑（PCTL）和连续随机逻辑（CSL）通常分别用于描述离散时间和连续时间的概率属性规范。在PCTL和CSL中，执行满足某些时态性质的可能性可以通过其基本计算树逻辑（CTL）中路径量词的概率扩展来定量表示，但它们的路径公式在CTL中是通过相同的运算符来表示的。由于这个原因，它们都不能表示具有定量时间属性的公式，例如“某些属性在路径上超过80%的时间点（在某个有界区间内）保持不变”的形式。本文引入了一个新的时态算子来表达事件频率的概念，并在CTL \star的基础上定义了概率频率时态逻辑（PFTL）。因此，我们可以很容易地表示概率系统中的行为的时间属性。然而，它是很难开发一个完整的PFTL模型检查，由于丰富的表现力。相应地，我们开发了一个模型检测算法的CTL类片段的PFTL对有限状态马尔可夫链，和一个近似的模型检测算法的有界线性时序逻辑（LTL）类片段的PFTL对可数状态马尔可夫链。
Unifying Hyper and Epistemic Temporal Logic
在文献中，已经提出了两个强大的时序逻辑形式主义表达信息流的安全性要求，在一般情况下，超越常规的属性。一个是经典的，基于认知逻辑的知识模态。另一个，所谓的超逻辑，是最近的，包括许多建议，从文献中，它是基于明确的和同时量化多个路径。为了更好地理解这些逻辑如何相互比较，我们考虑了逻辑KCTL*（CTL* 的知识模态和同步完美回忆语义的扩展）和HyperCTL*。我们首先确定KCTL* 和HyperCTL* 在表达上是不可比的。其次，我们引入并研究了HyperCTL* 的自然线性过去扩展，以统一KCTL* 和HyperCTL*;事实上，我们表明KCTL* 可以很容易地在线性时间内转换为所提出的逻辑。此外，我们证明了这种新的逻辑的模型检测问题是可判定的，我们提供了它的确切的计算复杂性方面的一个新的措施的路径量词的交替。为此，我们解决了开放的复杂性问题，无限制的量化命题时序逻辑。
Exploring the Jungle of Intuitionistic Temporal Logics
本文探讨直觉主义时序逻辑的公理系统，证明其在克里普克框架或动态拓扑系统上的可靠性，并区分七种不同逻辑。
Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
一阶时态逻辑因其糟糕的计算行为而臭名昭著。众所周知，即使是两个变量的一元片段在各种线性时间线上也是高度不可判定的，并且在分支时间上，即使是一个变量的片段也可能是不可判定的。然而，已经有几个试图找到良好的一阶时序逻辑和相关的时序描述逻辑的片段，主要是通过限制可用的量词模式，或考虑子布尔语言。在这里，我们分析看似“温和”的扩展可判定的一个变量的片段与计数能力，解释模型与恒定，减少，扩大一阶域。我们表明，在大多数类的线性订单，这些逻辑是（有时高度）不可判定的，即使没有常数和函数符号，并与唯一的时间运营商“最终”。我们建立连接与双峰逻辑在二维产品结构具有线性和“差异”（不等式）组件的关系，并证明我们的结果在此双峰设置。我们给出了一个普遍的结果，即许多具有可交换线性和差分关系的双峰模型的可满足性是不可判定的。作为一个副产品，我们还获得了新的例子，但Kripke不完全双峰逻辑的axiomatisable。我们的结果推广了双峰逻辑在两个线性关系的乘积上的类似下界，并且我们的证明方法与这些结果的证明有很大的不同。与以前的证明，第一个“对角编码”的无限网格，然后使用减少平铺或图灵机的问题，在这里，我们直接使用的网格状结构的产品框架，并获得undecidability减少计数器（明斯基）机的问题。
A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time
区间时态逻辑（Interval Temporal Logic，ITL）是一种用于时间段推理的时态逻辑。25年来，国际交易日志以多种方式得到应用，并对若干国际交易日志变体、公理系统和工具进行了研究。我们解决了长期以来的开放问题，找到一个完整的公理系统的基本量词自由命题ITL（PITL）的无限时间分析非终止计算系统。我们的完整性证明使用减少到完整的PITL有限时间和传统的命题线性时间时序逻辑。与非初等计算复杂性同样表达逻辑的完整性证明不同，我们的语义方法不使用表格，子公式关闭或明确的演绎涉及编码的欧米茄自动机和非平凡的技术，以补充它们。我们相信，我们的结果也提供了基于区间推理的自然性的证据。
First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic
我们调查基于本体的数据访问时态数据。我们考虑在离散时间（Z，<）上解释的线性时态逻辑LTL中给出的时态本体。在LTL或MFO（<）中给出，一元一阶逻辑具有内置的线性顺序。我们关心的是一阶重写本体介导的查询（OMQs）组成的时间本体和查询。通过考虑本体中使用的时态运算符并区分完整LTL及其核心Krom和Horn片段中给出的本体，我们通过证明可重写为FO（<），具有内置线性顺序的一阶逻辑或FO（<，E），对于任何固定的n > 1，它用标准算术谓词扩展FO（<），说“x等于0模n”，或者FO（RPR），它用关系原语递归扩展FO（<）。就电路复杂性而言，FO（<，E）和FO（RPR）可重写性分别保证OMQ在统一AC 0和NC 1中应答。我们获得了类似的层次结构更有表现力的查询类型：积极的LTL-公式，单调MFO（<）-和任意MFO（<）-公式。我们的研究结果是直接适用的，如果要访问的时态数据是一维的，而且，他们奠定了基础，调查基于本体的访问使用组合的时间和描述逻辑在二维时态数据。
Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
路径检查是模型检验问题的一种特殊情况，其中所考虑的模型是单个路径，在监视、测试和验证中起着重要的作用。我们证明了线性时间时序逻辑（LTL），路径检查可以有效地并行化。除了核心逻辑，我们考虑扩展的LTL与有界未来（BLTL）和过去的时间（LTL+过去）运营商。尽管这两个扩展都以指数方式提高了逻辑的简洁性，但路径检查仍然可以有效地并行化：我们对LTL、LTL+Past和BLTL+Past的算法是在AC ^1（logDCFL）\subseteq NC中。
Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems
本文给出了区间时态逻辑（ITL）和持续时间演算（DC）在无穷区间上的概率扩展，并给出了它们的完整的希尔伯特式证明系统。的完整性结果是一个强完备性定理的概率ITL系统相对于一个抽象的语义和相对完备性定理的概率DC系统相对于实时语义。所提出的系统subconsiderable概率实时DC从文献中已知的。所提出的系统之间的对应关系和系统的概率区间时态逻辑有限的时间间隔和扩展模态。
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-完全的，即，对于这些逻辑，只有一个变量的公式的可满足性与任意公式的可满足性一样困难。
Relaxing safety for metric first-order temporal logic via dynamic free variables
我们定义了一个片段的度量一阶时态逻辑公式，保证其表表示的有限性。我们扩展我们的片段的定义，以涵盖时间的双重运营商触发和释放，并表明我们的片段是严格大于以前在文献中使用的。我们将这些添加到现有的运行时验证工具，并正式验证在伊莎贝尔/HOL的工具正确输出的常数表，满足监控公式。最后，我们提供了一些示例规范，由于我们的贡献，这些规范现在是可监控的。
A Theory of Sampling for Continuous-time Metric Temporal Logic
本文回顾了经典的概念，采样的实时时序逻辑的建模和分析系统的设置。研究了度量时态逻辑（MTL）公式在连续时间模型和离散时间模型上的可满足性之间的关系。它示出在何种程度上通过采样连续时间信号获得的离散时间序列捕获的语义MTL公式在两个时域。主要结果适用于“平”的公式，不嵌套的时间运营商，并可以适用于减少验证问题MTL在连续时间模型的问题，在离散时间相同的问题，从而在一个自动化的部分实际有效的离散化技术。
RobTL: A Temporal Logic for the Robustness of Cyber-Physical Systems
我们提出了鲁棒性时序逻辑（RobTL），一种新的时序逻辑的规范和分析的行为之间的距离的网络物理系统（CPS）在有限的时间范围内。与表达系统行为属性的经典时态逻辑不同，我们可以使用RobTL规范来度量系统在不同目标和时态约束下的行为差异，并研究这些差异如何随时间演变。由于CPS的行为不可避免地受到不确定性和近似，我们展示了RobTL的独特功能如何使我们能够指定系统对扰动的鲁棒性，即，它们即使在扰动的影响下也能正常工作的能力。由于CPS的概率性质，我们的模型检验算法的RobTL规格是基于统计推断。作为我们的框架的应用程序的一个例子，我们认为一个监督，自我协调的引擎系统，是受攻击的目的是造成设备的过度压力。
The Complexity of Learning Temporal Properties
本文研究LTL、CTL和ATL时序逻辑被动学习问题的计算复杂性，证明无界二元运算符情况下均为NP完全，并揭示有界情况下不同逻辑间的复杂性差异。
Model-checking Counting Temporal Logics on Flat Structures
我们研究了几个扩展的线性时间和计算树的时间逻辑与量词，允许计数经常某些属性举行。对于大多数这些扩展，模型检验问题是不可判定的，但我们表明，可判定性可以恢复考虑平坦的Kripke结构，每个状态属于最多一个简单的循环。大多数决策程序是基于（平面）计数器系统的结果，其中计数器用于实现计数运算符的评估。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。