A quantitative extension of Interval Temporal Logic over infinite words
Halpern和Shoham的区间时态逻辑HS的模型检验最近已经被系统地研究，并且已知它在三种不同的语义（基于状态、基于迹和基于树的语义）下是可判定的。在这里，我们专注于基于轨迹的语义，其中的主要语义实体是无限的执行路径（轨迹）的给定Kripke结构，假设在另外的同质性的命题估值。我们引入了一个定量的扩展HS的痕迹，称为差异HS（DHS），允许一个表达时间间隔长度（持续时间）之间的差异的限制。一些模态的定量扩展直接导致不可判定性，因此，我们通过考虑DHS的严格语法片段来研究模型检验和可满足性问题的可判定性边界。特别是，我们确定了最大的可判定的片段DHSS的DHS证明，此外，所考虑的问题的片段至少是2EXPSPACE硬。此外，通过利用新的结果，线性时间混合逻辑，我们表明，对于一个同样具有表现力的片段的DHSS，问题是EXPSPACE完全的。最后，我们通过一个新的混合逻辑的单变量片段提供了一个表征HS的痕迹。
2022-07-13 cs.LO
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
Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete
在表达性和复杂性之间选择正确的折衷是区间时态逻辑的主要问题。在他们的开创性论文中，Halpern和Shoham表明HS（艾伦关系的时序逻辑）的可满足性问题在任何合理的线性序类上都是高度不可判定的。为了恢复可判定性，可以限制时间模态的集合和/或模型的类别。在下文中，我们专注于HS片段在同质性假设下的可满足性问题，根据该假设，任何命题字母在区间上成立，如果它在所有点上成立。具有齐次性的完全HS问题已经被证明是非初等可判定的，但它唯一已知的下界是EXPSPACE（事实上，对于前缀和后缀BE的逻辑已经证明了EXPSPACE-困难，这是它的一个非常小的片段。本文证明了将Allen关系Meets加到BD上使BD成为EXPSPACE完备的。
2021-09-17 cs.LO
The Logic of Prefixes and Suffixes is Elementary under Homogeneity
针对同质性假设下区间时序逻辑 BE 的有限可满足性问题，提出有界嵌套模态的等可满足范式，证明其复杂性为 EXPSPACE 完全。
2023-04-22 cs.LO
Dyck algebras, interval temporal logic and posets of intervals
研究了等长Dyck路集合上的一种自然Heyting代数结构。给出了伪补运算、相对伪补运算以及正则元素的几何描述。我们还发现这样的海廷代数，我们称之为戴克代数的逻辑理论解释，通过显示它们是一个经典的区间时态逻辑（也称为Halpern-Shoham逻辑）的某个片段的代数对应。最后，我们提出了一个推广我们的方法，提出了类似的研究所产生的Heyting代数的偏序集的区间的有限偏序集使用Birkhöff对偶。为了说明这一点，我们展示了几个组合参数的Dyck路径可以表示的Heyting代数结构的Dyck代数连同一定的总秩序的原子集的每个Dyck代数。
2015-03-17 cs.DM cs.LO math.CO
Model Checking the Logic of Allen's Relations Meets and Started-by is $P^NP$-Complete
在Halpern和Shoham的时间间隔模态逻辑（HS）的大量片段中，Allen的关系Meets和Started-by的逻辑AB处于中心位置。在某些时间间隔上可能为真的陈述，但在它们的子时间间隔上不为真，例如成就，以及关于时间间隔长度的度量约束，例如，强制时间间隔至少为（分别为，最多，正好）k点长，可以用AB表示。此外，在自然数N的线性顺序上，它包含（基于点的）逻辑LTL，因为它可以容易地编码下一个和直到模态。最后，它的表现力足以捕获ω-正则语言，即对于每个ω-正则表达式R，存在一个AB公式，使得由R定义的语言与N上的的模型集一致。已经证明N上AB的可满足性问题是EXPSPACE-完全的。本文证明了在齐性假设下，它的模型检验问题是Δ^p_2 = P^NP-完全的（为了比较，完全HS的模型检验问题是EXPSPACE-困难的，唯一已知的判定过程是非初等的）.此外，我们还证明了Allen关系Met-by的模态可以被添加到AB上而不需要额外的代价（AA 'B也是P^NP-完全的）。
2016-09-14 cs.LO
Interval-based Synthesis
我们介绍了Halpern和Shoham的模态逻辑的时间点上的等价关系扩展的间隔，简称HSeq的综合问题。类似于一个后继者的一元二阶逻辑的情况，所考虑的合成问题接收HSeq公式phi和命题变量和时间请求的有限集合Sigma作为输入，并且它确定对于每个区间结构中的Sigma中的元素的所有可能的评估，存在对剩余的命题变量和时间请求的评估，使得所得到的结构是Φ的模型。我们将注意力集中在HSeq的一些有意义的片段的合成问题的可判定性上，其模态来自集合A（满足），Abar（满足），B（开始），Bbar（开始），在有限的线性顺序和自然数上解释。我们证明了片段ABBbareq是可判定的（非原始递归硬），而片段AAbarBBbar原来是不可判定的。此外，我们表明，即使ABBbar的合成问题变得不可判定，如果我们用自然数取代有限的线性订单。
2014-08-26 cs.FL cs.LO
Epistemic Logic of Know-Who
Claremont McKenna College（克莱蒙特·麦肯纳学院）；King’s College（国王学院）
本文建议使用Grove-Halpern名称语义学将"知道谁"定义为一种情态。它还介绍了一个逻辑系统，描述了模态之间的相互作用"知道谁"，"知道"，"为所有代理人"。主要的技术成果是所提出的系统的完整性定理。
2021-03-03 cs.AI cs.LO
Interval vs. Point Temporal Logic Model Checking: an Expressiveness Comparison
近年来，基于区间时态逻辑的模型检验作为基于标准点时态逻辑（如LTL、CTL、CTL* 等）的模型检验的可行替代方案而出现。像往常一样，系统的行为通过（有限）Kripke结构来建模。然而，虽然被解释为“逐点”的时间逻辑描述了系统如何逐状态地演变，以及系统状态的谓词属性，但那些被解释为“逐区间”的时间逻辑表达了计算延伸的属性，跨越了一系列状态。假设一个命题字母在一个计算延伸（间隔）上保持不变，当且仅当它在每个分量状态上保持不变（同质性假设）。一个自然的问题出现了：用间隔代替点作为主要的时间实体有什么好处，或者这只是一个品味问题？本文研究了Halpern和Shoham的区间时态逻辑（HS）在模型检验中的表达能力，并与LTL、CTL和CTL* 进行了比较。为此，我们考虑HS的三种语义变体：基于状态的变体，由Montanari等人引入，它允许时间在过去和将来都分支，基于计算树的一个，它只允许时间在将来分支，基于轨迹的变体，它不允许时间分支。这些变体相互比较，并与上述标准逻辑进行比较，得到一个完整的画面。特别是，我们表明，HS与跟踪为基础的语义是相当于LTL（但至少指数更简洁），HS与计算树为基础的语义是相当于有限的CTL*，和HS与基于状态的语义是无法比拟的所有这些（LTL，CTL和CTL*）。
2018-09-24 cs.LO
Checking Interval Properties of Computations
模型检验是形式化验证中广泛采用的一种有效方法。给定一个系统的模型，例如，Kripke结构和指定其预期行为的公式，可以通过对照模型检查公式来验证系统是否满足行为。传统上，系统行为由时序逻辑的公式表示，例如LTL等。这些逻辑是“逐点”解释的，因为它们描述了系统如何逐状态演化。然而，有相关的属性，如那些约束时间扩展事件对之间的时间关系或涉及时间聚合，这是固有的“基于间隔”，因此要求一个时间间隔逻辑。本文给出了区间逻辑环境下的模型检验问题的形式化描述。首先，我们提供了一个解释公式的Halpern和Shoham的时间间隔逻辑HS有限Kripke结构，它允许一个检查计算的时间间隔属性。然后，证明了有限Kripke结构下HS的模型检验问题是可判定的，并给出了其计算复杂性的一个下界.
2016-01-13 cs.CC cs.LO
Begin, After, and Later: a Maximal Decidable Interval Temporal Logic
University of Verona（维罗纳大学）；University of Murcia（穆尔西亚大学）
区间时态逻辑（Interval Temporal Logic，ITL）是用于对在区间上表达的时态语句进行推理的逻辑，即，一段时间。到目前为止，最著名的ITL研究是Halpern和Shoham的HS，这是十三个Allen间隔关系的逻辑。不幸的是，HS和它的大多数片段都有一个不可判定的可满足性问题。这阻碍了这一领域的研究，直到最近，当一些非平凡的可判定的ITL已经被发现。本文是对HS所有不同片段的完整分类的贡献。我们考虑区间关系Begins、After、Later及其逆Abar、Bbar和Lbar的不同组合。我们从以前的作品中知道，ABBbarAbar组合只有在考虑有限域时才是可判定的（在其他地方是不可判定的），并且ABBbar在自然数上是可判定的。我们扩展这些结果表明，ABBar的可判定性可以进一步扩展到捕获的语言ABBbarLbar，这奠定了ABBar和ABBbarAbar之间，原来是最大的w.r.t强离散线性订单（例如有限订单，自然，整数）的可判定性。我们还证明了建议的决策过程是最佳的复杂性类。
2010-06-08 cs.AI cs.LO
The addition of temporal neighborhood makes the logic of prefixes and sub-intervals EXPSPACE-complete
本文研究 chop 区间时序逻辑弱化片段 $\mathsf{BD}_{hom}$ 添加时间邻域模态 $A$ 后的扩展，证明所得逻辑 $\mathsf{BDA}_{hom}$ 的可满足性问题为 EXPSPACE-完全，表明该扩展同时提升了表达能力和计算复杂度。
2024-03-21 cs.LO
Tableau-based decision procedure for full coalitional multiagent temporal-epistemic logic of linear time
我们开发了一个基于表格的决策过程的充分联盟的多智能体的时间认知逻辑的线性时间CMATEL（CD+LT）。它扩展了LTL与运营商的共同和分布式知识的所有联盟的代理。Tableau程序以指数时间运行，与Halpern和Vardi为我们的逻辑片段获得的下限相匹配，从而为CMATEL（CD+LT）提供了一个复杂性最优的决策程序。
2019-11-21 cs.LO cs.MA
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
Model checking: the interval way
[...]最著名的模型检验（MC）技术是从80年代后期发展起来的，记住著名的“基于点”的时序逻辑LTL和CTL。然而，虽然这种逻辑的表达能力是毋庸置疑的，但我们可能希望检查系统模型的一些属性，这些属性本质上是“基于区间的”，因此不能用基于点的时间逻辑来表达，例如，“命题P必须在给定计算扇区中至少保持平均数量的系统状态”。在这里，时间间隔逻辑（ITLs）开始发挥作用，为时间推理提供了另一种设置。这样的逻辑处理间隔，而不是点，作为它们的原始实体：这一特征使它们能够表达时间属性，例如持续时间的动作，成就和时间聚合，这在标准的基于点的逻辑中无法处理。Halpern和Shoham的时间间隔模态逻辑（HS）是最著名的ITL之一：除了相等之外，它为间隔对之间的13种可能的排序关系中的每一种提供了一种模态。在这篇论文中，我们的注意力集中在基于HS的MC，在属性规约语言的角色，这是一个小的工作已经做了比较MC基于点的时态逻辑。我们研究了这种问题的复杂性，考虑不同的系统模型，我们也比较了HS的表达能力，在MC的LTL，CTL和CTL*。[...]
2019-02-11 cs.CC cs.LO
Applications of Interval-based Temporal Separation: the Reactivity Normal Form, Inverse $Π$, Craig Interpolation and Beth Definability
Institute of Mathematics and Informatics（数学与计算机科学研究所）；Bulgarian Academy of Sciences（保加利亚科学院）
本文通过区间基于的时间分离技术，展示了如何简洁证明反应正常形式、逆Π、Craig插值和Beth可定义性等关键结果。
2026-02-11 cs.LO
Temporal Ensemble Logic
McGovern Medical School（麦戈文医学院）；McWilliams School of Biomedical Informatics（麦克威廉姆斯生物医学信息学院）；Texas Institute for Restorative Neurotechnologies（德克萨斯修复神经技术研究所）；The University of Texas Health Science Center at Houston（德克萨斯大学休斯顿健康科学中心）
本文提出时序集成逻辑 TEL，用于形式化生物医学中的线性时间时序推理，重点研究离散时间版本 TEL_N+ 的语义、证明系统、不可判定性及表达力，弥补现有逻辑框架在严谨性与表达力之间的不足。
2024-08-30 cs.AI cs.FL cs.LO
