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
Logic for conditional strong historical necessity in branching time and analyses of an argument for future determinism
本文提出分支时间中条件性强历史必然性的逻辑，用于分析未来决定论论证，并指出该论证在此逻辑下不成立。
2024-05-24 cs.LO
A DPLL Procedure with Dichotomous Branching for Propositional Product Logic
针对命题乘积逻辑，提出基于二分支的 DPLL 过程修改版本，证明其反驳可靠性与有限完备性，为模糊推理与自动演绎结合提供解决方案。
2023-10-24 cs.LO
Characterizing Weighted MSO for Trees by Branching Transitive Closure Logics
我们引入了分支传递闭包算子的加权一元二阶逻辑公式的分支对应于一个自然的方式在树中固有的分支。对任意交换半环，我们证明了树上的加权一元二阶逻辑等价于由下列算子之一开始的公式的可定义性：（i）分支传递闭包或（ii）存在二阶量词后接泛一阶量词;在这两种情况下，该运算符被应用于（a）通过模计数而丰富的布尔一阶逻辑或（b）布尔一元二阶逻辑上的步进公式。
2015-04-29 cs.FL cs.LO
Hybrid Branching-Time Logics
混合分支时间逻辑被引入作为状态变量和向下箭头绑定器的CTL类逻辑的扩展。根据最近的工作在线性框架，只有一个单一的变量逻辑被认为是。研究了结果逻辑的表达能力和可满足性的复杂性。作为主要结果，证明了几个分支时间逻辑的混合形式的可满足性问题是2 EXPTIME-完全的。这些分支时间逻辑的范围从CTL的严格片段到CTL的扩展，可以谈论过去并表达公平性。相对于CTL的复杂性差距解释了相应的简洁性结果。为了证明这个上界，将分支时间逻辑的自动机理论方法推广到混合逻辑，证明了交替单卵石Buchi树自动机的非空性是2 EXPTIME-完全的。
2007-08-13 cs.CC cs.LO
A new face of the branching recurrence of computability logic
这封信介绍了可计算性逻辑的分支递归操作的一个新的、实质上简化的版本（见http：//www.cis.upenn.edu/casigiorgi/cl.html），并证明了它与旧的“规范”版本的等价性。
2011-11-21 cs.LO math.LO
Logic and Branching Automata
在本文中，我们研究的逻辑方面的分支自动机，定义Lodaya和韦尔。我们首先证明了分支自动机所识别的有限N-自由偏序集的语言类在补下是闭的。然后，我们定义了一个逻辑，命名为P-MSO，因为它是一元二阶逻辑与Presburger算法的扩展，并表明它是精确的表达分支自动机。由于一种形式主义从另一种形式主义构造的有效性，所有有限N-自由偏序集类的P-MSO理论是可判定的。
2015-10-14 cs.FL cs.LO
Learning Branching-Time Properties in CTL and ATL via Constraint Solving
本文研究从Kripke结构和并发博弈结构样本中学习CTL与ATL公式的问题，通过将学习问题编码为可满足性问题并结合不动点模型检测算法进行符号化求解，并在Python原型中验证了方法的有效性。
2024-06-28 cs.LO
Non-Elementary Complexities for Branching VASS, MELL, and Extensions
我们研究了向量加法系统的分支扩展上的可达性问题的复杂性，这使我们能够推导出命题线性逻辑的片段和变体的新的非初等复杂性界。我们证明了乘法指数片段的可证明性在仿射情况下已经是塔硬的，因此是非初等的。我们匹配这个下界的充分命题仿射线性逻辑，证明其塔完全性。我们还证明了命题压缩线性逻辑的可证性是阿克曼完备的。
2022-05-16 cs.LO
Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
本文扩展Outcome Logic，以选择的代数表示统一刻画非确定性、概率性等分支效应，并给出支持通用循环、可跨规范复用证明片段的较完整证明系统及其元理论。
2025-06-10 cs.LO cs.PL
On the Complexity of Branching-Time Logics
我们分类的可满足性问题的CTL和UB的扩展的复杂性。我们考虑的扩展是路径公式，公平性，过去的模态和过去的布尔组合。我们的主要结果表明，所有这些扩展的CTL的可满足性仍然是在2-EXPTIME，这与CTL* 的非初等复杂性与非初等复杂性的强烈对比。我们给出了一个完整的分类，这些扩展的组合，产生一个二分法的扩展与2-EXPTIME完全和那些EXPTIME完全的复杂性。特别是，我们表明，可满足性的UB扩展与过去是完整的2-EXPTIME，矛盾的要求，一个更强的逻辑文献。利用一种新的卵石自动机建立了上界。
2009-06-14 cs.LO
The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
本文研究了在 van Glabbeek 分支时间谱中，判定有限无环过程特征公式的复杂度，给出了可满足性与素性问题的复杂度结果，并探讨了多项式时间可解与计算困难的逻辑边界及公式构造的复杂度。
2024-11-13 cs.LO
Deciding characteristic formulae: A journey in the branching-time spectrum
Reykjavik University（雷克雅未克大学）；Gran Sasso Science Institute（格兰萨索科学研究所）
本文研究了在van Glabbeek分支时间谱中各逻辑中判定公式是否为特征公式的问题，分析了可满足性和素性问题的复杂性，并探讨了多项式时间与(co)NP或PSPACE完全问题之间的边界。
2026-03-26 cs.LO
Adventures in Monitorability: From Branching to Linear Time and Back Again
本文建立了一个全面的Hennessy-Milner逻辑与递归，一个非常有表现力的变种模态$μ$演算的运行时监控性理论。它调查的可监测性，逻辑与线性时间语义，然后比较所获得的结果与以前在文献中提出的分支时间设置。我们的工作建立了一个表达层次的Hennessy-Milner逻辑递归的可监控片段的线性时间设置，并确切地确定了什么样的保证，可以使用运行时监视器的层次结构中的每个片段。每个片段被证明是完整的，在这个意义上，它可以表达所有的属性，可以在相应的保证下进行监控。该研究是使用一个原则性的方法来监测连接的逻辑和操作语义的监视器的语义。建议的框架支持自动合成正确的监视器从可监视的属性。
2019-02-01 cs.LO
Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
本文综述了近年来通过符号模型检验验证时态认知逻辑的一些工作，重点介绍了基于OBDD和基于SAT的离散和实时分支时态逻辑的认知逻辑验证方法。
2007-09-04 cs.LO
On the Expressive Power of the Normal Form for Branching-Time Temporal Logics
随着涉及复杂分布式系统的新兴应用，分支时间规范特别重要，因为它们反映了此类应用的动态和非确定性。我们描述了一个简单而强大的分支时间规范框架的表达能力-分支时间范式（BNF），它已被开发为分支时间时序逻辑的子句解析的一部分。我们显示的编码的布奇树自动机的语言的范式，从而表示，语法，树自动机在一个高层次的方式。因此，我们可以把BNF作为后者的范式。这些结果使我们能够（1）将给定的问题规格转换为范式，并作为一种验证方法的演绎推理技术-小句的时间分辨率;（2）适用于解决方法的核心组成部分之一-循环搜索提取，句法，隐藏的不变量在广泛的复杂的时间规格。
2022-04-14 cs.FL cs.LO
Graded Monads and Graded Logics for the Linear Time -- Branching Time Spectrum
并发系统的基于状态的模型传统上被认为是在各种概念下的进程等价。在标记的过渡系统的特定情况下，这些等价的范围从跟踪等价（强）的双相似性，并组织在什么是所谓的线性时间分支时间谱。通用的共代数和分级单子的组合提供了一个通用的框架，在该框架中，并发的语义可以参数化的分支类型的底层过渡系统和粒度的进程等价。我们表明，在本文件中，这一框架的分级语义subanimate最重要的等价物从线性时间分支时间谱。分级语义的一个重要特征是它允许特征模态逻辑的原则性提取。我们已经建立了这些分级逻辑的不变性下，在早期的工作中给定的分级语义，在本文中，我们扩展了逻辑框架与一个明确的命题层，并提供了一个通用的表达标准，概括了经典的亨尼西-米尔纳定理粗糙的概念过程等价。我们提取分级逻辑的一系列分级语义标记的过渡系统和概率系统，并给出示例性的证明，他们的表现力的基础上，我们的通用标准。
2020-10-20 cs.LO math.CT
On the proof complexity of logics of bounded branching
研究了基本传递模态逻辑（K4，S4，GL，.）的扩展弗雷格（EF）系统的证明复杂性。用有界分支公理$\mathbf{BB}_k$扩充。首先，我们研究了这些逻辑的EF系统中的析取属性和更一般的扩展规则的可行性：我们表明，相应的决策问题减少到总coNP搜索问题（或等价地，不相交的NP对，在二进制的情况下）;更确切地说，扩展规则的决策问题等价于经典EF系统的插值的某种特殊情况。接下来，我们使用这个特征证明超多项式（甚至指数，更强的假设）之间的EF和替代弗雷格（SF）系统的所有传递逻辑包含在$\mathbf{S4.2GrzBB_2}$或$\mathbf{GL.2BB_2}$的一些假设下弱于$\mathrm{PSPACE \ne NP}$分离。我们还证明了类似的结果超直觉逻辑：我们的特点的多结论维瑟规则的决策复杂性在EF系统的Gabbay-德容逻辑$\mathbf T_k$，我们显示EF和SF之间的条件分离的所有中间逻辑$\mathbf{T_2 + KC}$。
2022-05-16 cs.LO math.LO
Separating the basic logics of the basic recurrences
本文表明，即使在最基本的水平上，并行，可数分支和不可数分支递归的可计算性逻辑（见http：//www.cis.upenn.edu/caugiorgi/cl.html）验证不同的原则。
2011-11-15 cs.LO math.LO
Strategies, model checking and branching-time properties in Maude
本文扩展Maude模型检验能力，使其支持策略控制系统上的CTL*和μ-演算分支时间性质验证，并通过通用高效连接集成外部模型检验器并比较其性能。
2024-01-15 cs.LO
Computation Tree Logic with Deadlock Detection
研究了在没有下一状态模态的计算树逻辑（CTL-X）中满足相同公式的标号迁移系统的状态等价关系。这个关系是由De Nicola & Vaandrager通过将标记转移系统转化为Kripke结构而得到的，同时解除了对后者的总体性限制。他们将其描述为发散敏感分支互模拟等价。我们发现，这种等价未能成为一个交错并行组合的同余。原因是，CTL-X的非总Kripke结构的拟议应用缺乏表现力，以应付死锁属性是重要的，在并行组合的上下文中。我们提出了一个扩展的CTL-X，或替代治疗的非整体，填补这一空白。等价诱导我们的扩展的特点是分支互模拟等价与明确的分歧，这是，此外，示出的粗同余包含在分歧敏感的分支互模拟等价。
2009-12-22 cs.LO
Model Checking Stochastic Branching Processes
随机分枝过程是描述随机树的经典模型，在生物学、物理学和自然语言处理等领域有着广泛的应用。特别是，他们最近被提出来描述随机过程创建并行程序。本文考虑随机分支过程的模型检验问题。给定一个分支过程和一个确定性奇偶校验树自动机，我们感兴趣的是计算生成的随机树被自动机接受的概率。我们表明，这个概率可以与任何有理数在PSPACE，和0和1在多项式时间。在第二部分中，我们提出了逻辑PCTL的一个树扩展，并开发了一个PSPACE算法，用于对这个逻辑的公式进行分支过程的模型检验。我们还表明，该逻辑的定性片段可以在多项式时间内进行模型检查。
2012-06-06 cs.FL cs.LO
Reactive Synthesis: Branching Logics and Parameterized Systems
反应合成是一种自动的方法，可以将人类在某种逻辑中表达的意图转化为某种系统。本文分为逻辑和系统两部分。在第一部分中，我们开发了两种新的CTL* 合成方法。第一种方法由两个扩展的SMT为基础的有界综合：一个遵循自底向上的CTL* 模型检验，另一个遵循自动机框架。第二种方法将CTL* 合成减少为LTL合成。这种减少将任何LTL合成器变成CTL* 合成器。这两种方法已经实施，并可在网上查阅。在第二部分中，我们研究了两个系统架构的参数化综合。第一种体系结构是受缓存一致性协议启发的保护系统。在防护系统中，进程转换的启用或禁用取决于某些局部状态中是否存在其他进程。已有的关于保护协议的截断结果仅限于封闭系统，并且对于活性性质的应用有限。我们关闭这些差距，并证明了严格的截止与活性的开放系统，也截止检测死锁。第二种架构是令牌环系统，其中单个令牌循环布置在环中的进程。现有的参数化综合方法的实验表明，它不能扩展到大规格。首先，我们优化的方法，细化截止约简，使用模块化和抽象。评估显示了几个数量级的加速。其次，对工业仲裁协议AMBA进行了参数化综合案例研究。我们描述了新的技巧-一个新的截止扩展和分解合成-，再加上前面描述的优化，使我们能够合成AMBA在一个参数化的设置，第一次。
2018-08-28 cs.LO
The taming of recurrences in computability logic through cirquent calculus, Part I
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（现在的）第一部分包含了一个完整性证明和一个可靠性证明，（即将出版的）第二部分包含了一个完整性证明。
2012-09-19 cs.LO math.LO
The taming of recurrences in computability logic through cirquent calculus, Part II
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（前）第一部分包含了一个完整性证明，（现在）第二部分包含了一个完整性证明。
2011-06-19 cs.LO math.LO
Model-checking branching-time properties of probabilistic automata and probabilistic one-counter automata
本文研究概率自动机及概率一计数器自动机对 PCTL 与 PCTL$^*$ 的模型检测，通过归约空性问题并构造行为等价的一计数器自动机，证明两类问题均不可判定。
2021-08-30 cs.FL cs.LO math.LO
Positive Hennessy-Milner Logic for Branching Bisimulation
本文引入了 Hennessy-Milner 定理的有向版本，通过提出仅有限使用否定的正模态逻辑（PHMLU）和有向分支互模拟，证明了状态理论包含与有向互模拟的等价性，并揭示 HMLU 可由 PHMLU 的布尔组合表示。
2025-10-27 cs.FL cs.LO
One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics
本文首次用单一多维能量博弈统一刻画并判定带静默步的线性时间—分支时间谱系中从分支互模拟到弱迹等价的行为等价，并通过 Hennessy–Milner 逻辑的八个表达力维度建立正确性。
2024-11-21 cs.LO
Rich Counter-Examples for Temporal-Epistemic Logic Model Checking
模型检验验证系统的模型是否满足给定的属性，否则会产生一个反例来解释违规。验证的性质正式表示在时间逻辑。一些时态逻辑，如CTL，是分支的：它们允许表达关于模型的整个计算树的事实，而不是每个线性计算。当处理多模态逻辑时，这个分支方面甚至更加关键，即用几个转移关系表达系统事实的逻辑。一个突出的例子是CTLK，一个逻辑，原因的时间和认知属性的多智能体系统。一般来说，模型检查器为失败的属性生成线性反例，由模型的单个计算路径组成。但是一些分支性质只能通过一个线性反例来很好地和部分地解释。本文提出了更丰富的反例结构，称为树型注释反例（TLACE），属性的限制性CTL（ARCTL），CTL量化路径的扩展限制在动作标记的模型过渡。这些反例有一个分支结构，支持更完整地描述违反属性。这些反例的元素都注释了部分属性，以便更好地理解它们的结构。这些更丰富的反例的可视化和浏览成为一个关键问题，因为对于深度嵌套的属性，分支和状态的数量可以呈指数级增长。本文形式化地定义了TLACE的结构，刻画了TLACE的充分反例。模型和失效属性，并给出了ARCTL属性的生成算法。它还用CTLK中的例子说明了这种方法，使用CTLK到ARCTL的简化。所提出的方法已经实施，首先通过扩展NuSMV模型检查器来生成和导出分支反例，其次通过提供交互式图形界面来可视化和浏览它们。
2012-02-21 cs.LO cs.MA
Robust Computation Tree Logic
针对分支时间逻辑缺乏鲁棒语义的问题，提出采用多值语义的 rCTL 与 rCTL*，在保持或增强表达能力的同时，使模型检测、可满足性和综合复杂度不增加。
2023-10-24 cs.LO
Automaton-based Characterisations of First Order Logic over Infinite Trees
Università degli Studi di Napoli “Federico II”（那不勒斯费德里科二世大学）；Università degli Studi di Udine（乌迪内大学）
研究无限树上一阶逻辑的表达能力，引入两种犹豫树自动机，证明其精确捕捉了两种分支时间时序逻辑的表达能力，并揭示了一阶逻辑在该场景下的表达限制。
2026-10-28 cs.FL cs.LO
An Asynchronous Automata Approach to the Semantics of Temporal Logic
本文给出了描述异步自动机的微分方程并给出了它们的解x：R->{0，1}x. x{0，1}。对连续时间与离散时间的联系作了说明。连续时间和离散时间、线性时间和分支时间逻辑具有依赖于x的语义，它们的公式给出了自动机的性质。
2001-10-31 cs.LO
Paraconsistent Gödel modal logic on bi-relational frames
我们进一步发展了次协调哥德尔模态逻辑。在本文中，我们认为它的版本赋予Kripke语义的$[0,1]$值框架与两个模糊关系$R^+$和$R^-$（程度的信任断言和否认）和两个估值$v_1$和$v_2$（支持的真理和支持的虚假性）与德摩根否定$\neg$。我们证明了\emph{does not}是哥德尔模态逻辑的扩展，并且$\Box$和$\lozenge$是不可互定义的.我们还表明，几个重要的类的框架是$\birelKGsquare$可定义的（特别是，脆，单关系，和单分支）。对于多分支框架上的$\birelKGsquare$，我们建立了一个完备的约束表演算和一个基于该演算的判定过程，并利用该判定过程证明了$\birelKGsquare$在PSPACE中的可满足性和有效性.
2023-03-24 cs.LO math.LO
An Automaton-based Characterisation of First-Order Logic over Infinite Trees
本文研究无穷树上的一阶逻辑，通过引入两类犹豫树自动机精确捕获 polcCTLp 和 cCTL*[f] 的表达能力，提供自动机理论刻画并导出范式，揭示 FO 仅表达安全或共安全属性。
2025-09-17 cs.FL cs.LO
Higher Dimensional Modal Logic
高维自动机（HDA）是一种并发模型，可以表示大多数传统的偏序模型，如Mazurkiewicz迹，pomset，事件结构或Petri网。在Kripke结构上解释的模态逻辑是用于推理顺序行为和交叉并发的逻辑。模态逻辑是一阶逻辑的一个良好子集;模态逻辑的许多变体是可判定的。然而，对于更有表现力的HDA模型，没有类似模态的逻辑。在本文中，我们介绍和调查的模态逻辑HDAs，其中包括两个模态推理“期间”和“之后”。我们证明了这种一般的高维模态逻辑（HDML）是可判定的，并为它定义了一个公理系统，同时还说明了当HDA模型被限制为Kripke结构时，HDML的一个语法限制是如何成为标准模态逻辑的。然后，我们隔离类HDAs编码Mazurkiewicz痕迹，并显示如何HDML，与相应的直到运营商的自然定义，可以限制到LTrL（线性时间时序逻辑Mazurkiewicz痕迹）或分支时间ISTL。我们还研究了基本HDML语言wrt的表达能力。并得出结论，HDML捕获分裂互模拟。
2014-05-16 cs.LO
Stit Semantics for Epistemic Notions Based on Information Disclosure in Interactive Settings
我们使用分支离散时间结构上的STIT语义来表征四种类型的代理知识。它们是\emph{ex ante}知识、\emph{ex interim}知识、\emph{ex post}知识和专有技术。前三个概念来自于对决策过程中信息披露阶段的博弈论分析，第四个概念在行动逻辑和道义逻辑中都获得了突出地位，作为一种形式化能力的手段。近年来，人工智能领域的逻辑学家认为，任何关于责任归属和罪责的全面研究都应该包括对这类知识的适当处理。本文旨在澄清以前的尝试，正式在STIT逻辑，并提出替代的解释，在我们看来，更类似于STIT传统的责任研究。我们提出的逻辑使用扩展与知识运营商的Xstit语言，公式进行评估分支离散时间模型。我们还提出了一个公理系统的逻辑，并解决其健全性和完整性。
2019-11-19 cs.LO math.LO
Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
本文提出双向运行时强制执行框架，研究sHML安全属性的可执行性，并给出自动综合函数生成动作禁用监视器以保障系统正确性。
2023-02-27 cs.LO cs.PL cs.SE
Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
从计算复杂性的角度研究了分支时间逻辑CTL的可满足性问题。严格的上限和下限提供了每个时间操作符片段。在平行，最小模型的大小进行了研究，一个合适的概念极小。第三，研究了平坦的CTL，即，时态运算符嵌套深度非常低的公式。在复杂性和最小模型方面显示出尖锐的二分法：时间深度1具有低表达能力，而时间深度2相当于完整的CTL。
2017-02-24 cs.CC cs.LO
Responsibility and verification: Importance value in temporal logics
我们的目标是测量系统的一部分，它的能力，以满足规格的不确定性的选择的影响。为此，我们应用Shapley值的概念来验证作为一种手段来评估系统的一部分是多么重要。组件的重要性是通过将其控制权单独或与其他组件一起交给对手，并测试系统是否仍然可以满足规范来衡量的。我们研究这个想法的框架中的模型检查与各种经典类型的线性时间规范，并提出了几种方法来转置分支。我们还提供了严格的复杂性界限，几乎在每一种情况下。
2021-04-20 cs.LO
The Hierarchy of Hyperlogics
超性质通过将多个迹联系起来来推广迹的性质，在信息流安全中得到了广泛的研究。最近，已经提出了一些超性质的逻辑，并且需要理解它们的可判定性和相对表达性。新的逻辑已经从标准逻辑中获得了两个主要的扩展：时态逻辑，如LTL和CTL $^*$，已经通过为迹或路径添加变量而被推广到超属性。一阶逻辑和二阶逻辑，如一元一阶序逻辑和MSO，已经用等阶谓词扩展。我们研究了两个扩展的线性时间和分支时间逻辑的频谱的影响，特别是对命题的量化逻辑。由此产生的超逻辑层次结构与经典层次结构有很大不同，这表明等级别谓词比跟踪和路径变量增加了更多的表达能力。在超逻辑的层次结构中，我们确定了可满足性问题的可判定性的新边界。具体来说，我们表明，虽然HyperQPTL和HyperCTL $^*$都是不可判定的一般，公式内的$\exists^*\forall^*$片段是可判定的。
2020-05-12 cs.LO
Synchronous Team Semantics for Temporal Logics
University of Tübingen（蒂宾根大学）；Institut für Theoretische Informatik, Leibniz Universität Hannover（汉诺威莱布尼茨大学理论计算机科学研究所）；School of Computing Science, University of Glasgow（格拉斯哥大学计算科学学院）；Department of Computer Science, Aalborg University（奥尔堡大学计算机系）
本文为LTL和CTL提出团队语义，使其能表达超性质，研究其计算复杂度并证明带有团队语义的LTL是HyperLTL的可行替代方案。
2026-10-06 cs.LO
Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting
一阶时态逻辑因其糟糕的计算行为而臭名昭著。众所周知，即使是两个变量的一元片段在各种线性时间线上也是高度不可判定的，并且在分支时间上，即使是一个变量的片段也可能是不可判定的。然而，已经有几个试图找到良好的一阶时序逻辑和相关的时序描述逻辑的片段，主要是通过限制可用的量词模式，或考虑子布尔语言。在这里，我们分析看似“温和”的扩展可判定的一个变量的片段与计数能力，解释模型与恒定，减少，扩大一阶域。我们表明，在大多数类的线性订单，这些逻辑是（有时高度）不可判定的，即使没有常数和函数符号，并与唯一的时间运营商“最终”。我们建立连接与双峰逻辑在二维产品结构具有线性和“差异”（不等式）组件的关系，并证明我们的结果在此双峰设置。我们给出了一个普遍的结果，即许多具有可交换线性和差分关系的双峰模型的可满足性是不可判定的。作为一个副产品，我们还获得了新的例子，但Kripke不完全双峰逻辑的axiomatisable。我们的结果推广了双峰逻辑在两个线性关系的乘积上的类似下界，并且我们的证明方法与这些结果的证明有很大的不同。与以前的证明，第一个“对角编码”的无限网格，然后使用减少平铺或图灵机的问题，在这里，我们直接使用的网格状结构的产品框架，并获得undecidability减少计数器（明斯基）机的问题。
2015-06-08 cs.LO
On Propositional Dynamic Logic and Concurrency
University of Southern Denmark（南丹麦大学）
本文提出操作性命题动态逻辑(OPDL)，通过区分程序与轨迹，解决并发中交错捕捉问题，并扩展至CCS和编舞编程等并发模型。
2026-04-13 cs.LO
A More Sensitive Context
上下文行为逻辑（Logic of Behaviour in Context，LBC）是一种时空逻辑，用于表达连续状态过程的属性，如生化反应网络。LBC建立在现有的度量间隔时态逻辑（MITL）的基础上，并增加了一个“上下文模态”，探索系统与外部过程组成时的行为。LBC模型是连续π-演算（cπ）的术语，连续π-演算是一种具有连续状态空间的过程代数。我们以前发表的LBC模型检查技术需要检查过程行为轨迹上的许多点;并可能计算在每个这样的点上分支的进一步轨迹。这引起了两个困难：混合时间和空间模态可能需要计算大量的轨迹，其中微分方程的数值解是昂贵的;并且可能仍然不能检查这些轨迹上的离散点之间的中间值。在本文中，我们取得了进展，对这两个问题使用技术从信号时序逻辑和灵敏度分析。布尔信号积极地压缩轨迹信息，允许更有效的计算;灵敏度分析使我们能够通过计算较少数量的样本轨迹来可靠地检查区域上的公式。
2017-02-10 cs.LO
Model-checking Quantitative Alternating-time Temporal Logic on One-counter Game Models
我们考虑定量扩展的交替时间时序逻辑ATL/ATL称为定量交替时间时序逻辑（QATL/QATL），其中计数器的值可以比较使用等式，不等式和模约束的常数。我们解释这些逻辑在一个计数器的游戏模型，这是无限的持续时间的游戏有限的控制图，每个过渡可以增加或减少一个无界计数器的值。也就是说，这些游戏的状态空间通常是无限的。我们考虑的模型检验问题的逻辑QATL和QATL的一个计数器的游戏模型与VASS语义，我们开发的算法，并提供匹配的下界。我们的算法是基于减少的模型检验问题的模型检验游戏。这种方法使我们很容易处理扩展的逻辑语言以及无限的状态空间。该框架一方面概括了定性问题，如有限状态系统的ATL/ATL模型检验、单计数器过程上的分支时间时序逻辑CTL和CTL的模型检验以及LTL规范的可实现性问题。另一方面，QATL/QATL的模型检验问题推广了定量问题，如能源博弈（在QATL的情况下）和能源平价博弈（在QATL的情况下）的固定初始信用问题。我们的结果是积极的，因为我们表明，泛化是不是太昂贵的复杂性。作为一个副产品，我们获得了新的结果的复杂性模型检验CTL在一个计数器的过程中，并表明，决定赢家在一个计数器的游戏与LTL的目标是2 ExpSpace完成。
2014-09-19 cs.LO
A logic for temporal conditionals and a solution to the Sea Battle Puzzle
提出分支时间逻辑LTC形式化时间条件句推理，通过模型更新算子限制论域，解决海战谜题的宿命论结论，并给出可靠完备的公理化及归约到模态逻辑KD的判定算法。
2024-05-26 cs.LO
Cycle Detection in Computation Tree Logic
时态逻辑是一种非常强大的形式主义，在形式系统的设计和验证中得到了深入的研究和应用。它的应用通常简化为解决特定的决策问题，如模型检验和可满足性。在这类问题中，解决方案通常需要在循环中检测一些特定的属性。例如，当使用基于自动机、博弈论、SCC分解等的经典技术时，就会发生这种情况。令人惊讶的是，迄今为止，还没有一个时态逻辑被认为具有讨论循环的明确能力。在本文中，我们介绍周期-CTL *，经典的分支时间时序逻辑CTL* 的扩展，随着周期量化，以便在周期上的谓词。这个逻辑非常有表现力。事实上，我们证明，它严格扩展CTL*，是正交的μ演算。我们还提供了一些涉及非正则性质的例子，证明了它的有用性。我们研究了Cycle-CTL* 的模型检验问题，并证明了它和CTL* 一样是PSPACE完备的.我们还研究了逻辑的存在循环片段的可满足性问题，并证明了它在2 ExpTime中是可解的。这一结果利用了自动机理论的方法，以及新的ad-hoc定义的互模拟和树状展开。
2016-09-14 cs.FL cs.LO
Graded CTL Model Checking for Test Generation
最近，有一个很大的关注，从科学界对使用的模型检查技术作为一种工具，用于测试生成在仿真领域。本文旨在提供一个有用的手段，以获得更多的见解沿着这些路线。通过应用最近的研究成果在该领域的分级时序逻辑，我们提出了一个新的高效的模型检测算法分层有限状态机（HSM），一个建立良好的符号长期和广泛用于表示分层模型的离散系统。对使用分级时态逻辑表达的规范执行模型检查具有在唯一运行中返回更多反例的特性。我们认为这可以大大提高自动获取测试用例的效率。特别是，我们验证了两种不同的模型的HSM对分支时间的时间属性。
2011-11-09 cs.FL cs.LO
