Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking
下推系统（PDS）是递归程序的一种抽象模型，下推系统的模型检验方法已得到研究。寄存器PDS（RPDS）是由寄存器扩展的PDS，以有限的方式处理来自无限域的数据值。一个线性时序逻辑（LTL）模型检验方法已被提出的RPDS与定期估值，但该方法要求用于表示一个定期估值的寄存器自动机（RA）是向后确定的。本文提出了另一种方法来解决同样的问题，其中的模型检验问题的RPDS归结为PDS的问题，通过构造一个PDS互模拟等价于一个给定的RPDS。所提出的方法的结构比以前的模型检验方法更简单，不需要RA确定性或后向确定性，互模拟等价性清楚地保证了这种减少的正确性。另一方面，所提出的方法要求每个RPDS（和RA）具有新鲜度属性，其中每当RPDS用未存储在任何寄存器或栈顶中的数据值更新寄存器时，该值应该是新鲜的。本文还表明，这种模型检验问题的定期评估定义的一般RA是不可判定的，因此新鲜度约束是必要的，在所提出的方法。
2022-03-22 cs.FL cs.LO
Model-Checking of Linear-Time Properties Based on Possibility Measure
利用可能性测度研究了可能性Kripke结构下的LTL模型检验。首先介绍了可能性Kripke结构的概念和相关的可能性测度，然后研究了有限可能性Kripke结构线性时间可达性和重复可达性的模型检验.引入了可能性Kripke结构的标准安全性和非正则性，深入研究了正则安全性和非正则性的有限自动机验证问题。证明了有限可能性Kripke结构中正则安全性和非正则性的验证可以转化为本文所介绍的乘积可能性Kripke结构中可达性和重复可达性的验证。文中给出了几个算例来说明本文所提出的方法。
2016-09-25 cs.LO
Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions
认知Halpern-Shoham逻辑（EHS）是一种时间-认知逻辑，它将Halpern-Shoham逻辑的区间算子与认知模态相结合。EHS的语义是基于解释系统，其标签功能定义在区间的端点上。我们表明，这个定义可以概括为允许标签功能的基础上，整个区间的正则表达式。我们证明，所有已知的EHS的积极成果，特别是吸引人的复杂性，其模型检验问题的一些片段，仍然持有其推广。我们还提出了新的逻辑EHSre操作标准Kripke结构，并具有表达能力相当于EHS与正则表达式。我们比较EHSre的表达能力与标准的时间逻辑。
2015-09-02 cs.LO
Refinement Checking for Multirate Hybrid ZIA
混杂系统是一个既有离散分量又有连续分量的动态系统。为了研究混合系统的建模和验证问题，本文首先介绍了一种结合接口自动机、初始化多速率混合自动机和Z语言的规范化方法MZIA。同时，我们提出了一个加细关系MZIA。在此基础上，给出了有限域MZIA之间加细关系的检验算法，并证明了算法的正确性。
2014-10-13 cs.FL cs.LO
Tree Regular Model Checking for Lattice-Based Automata
树规则模型检验（TRMC）是分析无限状态系统的一系列技术的名称，其中状态由项表示，状态集由树自动机（TA）表示。TRMC的核心问题是判断一组坏状态是否可达。计算表示可达状态集合（的过近似）的TA的问题是不可判定的，但是存在基于树换能器的完成或迭代的有效解决方案。不幸的是，TRMC框架无法有效地捕获系统的复杂结构及其某些功能。作为示例，对于JAVA程序，项的结构主要用于捕获系统的状态的结构。相反，Java程序的整数必须用Peano数编码，这意味着任何代数运算都可能由数千个重写规则的应用程序表示。在本文中，我们提出了格树自动机（LTA），树自动机的扩展版本，其叶子配备了格。LTA允许我们表示可能无限的解释术语集。这些术语能够以有效的方式表示复杂的域和相关操作。我们还将经典的布尔运算扩展到LTA。最后，作为一个主要的贡献，我们引入了一个新的基于完成的算法计算可能无限的可达解释条款在有限的时间。
2012-03-07 cs.FL cs.LO
Symbolic model checking of tense logics on rational Kripke models
本文引入了有理Kripke模型类，研究了基本时态逻辑Kt的符号模型检验及其在该类模型中的一些扩展。有理Kripke模型基于（通常是无限的）有理图，顶点由某些正则语言中的单词标记，转换由异步双头有限自动机（也称为有理转换器）识别。在理性Kripke模型中，每个原子命题都在一组规则的状态中求值。证明了Kt的每个公式在每个有理Kripke模型中都有一个有效的可计算正则扩张，从而证明了有理Kripke模型中Kt的局部模型检验和全局模型检验是可判定的.这些结果被提升到Kt的一些扩展。我们研究并部分确定了模型检验过程的复杂性。
2008-10-30 cs.LO
Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
概率时间自动机（Probably Timed Automata，PTAs）是一种扩展了离散概率分布的时间自动机（Timed Automata，TA），它作为一种数学模型，广泛应用于随机和时间行为。在这项工作中，我们考虑的问题，模型检查的线性\emph{dense-time}性质在{PTA}。特别是，我们研究了线性密集时间属性，可以编码的TA与无限的验收criterion.First，我们表明，模型检查PTA对确定性TA规格的问题可以通过产品建设解决。基于乘积结构，证明了确定性TA规格问题的计算复杂性是EXPTIME-完全的。然后我们证明了当放宽到一般的（非确定性的）TA时，模型检测问题变得不可判定，我们的结果大大扩展了TA的稠密时间特性和非确定性。
2018-06-13 cs.FL cs.LO
Typestate Checking and Regular Graph Constraints
我们引入了正则图约束，并探讨其可判定性。规则图约束的动机是1）在存在链接的数据结构的情况下改变对象类型的类型检查，2）形状分析技术，以及3）在树和网格上的类似约束的泛化。我们定义了一个称为堆的图子类，作为程序在执行过程中构造的数据结构的抽象。证明了堆类上正则图约束蕴涵的有效性是不可判定的。我们表现出不可判定性表现出一定的“对应图”的存在和不存在的同态有限数量的固定图的特征。正则图约束蕴涵的不可判定性意味着，当这些属性用任何规约语言表达时，都没有算法来验证过程前提条件是否满足，或者不变量是否保持不变，至少与正则图约束一样具有表达性。
2004-08-05 cs.LO cs.PL
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems (technical report)
我们提出了一个通用的框架，建模和验证的认识属性参数化的多智能体系统，通过真实的公告进行通信。在我们的框架中，代理的数量或某些资源的数量被参数化（即先验未知），相应的验证问题询问给定的认知属性是否为真，而不管参数的实例化。例如，在一个泥泞的儿童拼图中，人们可以问每个孩子是否最终都会发现他是否泥泞，而不管孩子的数量。我们的框架是定期模型检验（RMC）为基础的，其中同步有限状态自动机（相当于一元二阶逻辑的话）被用来指定系统。我们提出了一个公共声明逻辑的扩展作为规约语言。特别感兴趣的是增加了所谓的迭代公共公告运营商，这是至关重要的推理知识参数化系统。虽然运营商的模型检验问题不可判定的，我们表明，这成为一个适当的“消失关系”时，可判定的。此外，我们展示了如何Angluin的L* 算法学习有限自动机可以应用到找到一个消失的关系，这是保证终止，如果它是正规的。我们已经实现了该算法，并将其应用于这样的例子，如泥泞的儿童拼图，俄罗斯卡问题，大数挑战。
2021-03-08 cs.FL cs.LO cs.MA
On (Omega-)Regular Model Checking
检查无限状态系统通常通过将无限状态集编码为正则语言来完成。计算这样一个规则的表示，比如说，一个系统的可达状态集需要加速技术，可以计算无限数量的转换的效果。在已经提出的加速技术中，可以找到特定的和通用的技术。特定技术利用被分析的特定类型的系统，例如，操纵队列或整数的系统，而通用技术仅假设转换关系由有限状态转换器表示，其必须迭代。在本文中，我们调查的可能性，使用通用技术的情况下，只有特定的技术已被利用到目前为止。发现现有的通用技术往往是不适用的情况下，很容易处理的特定技术，我们已经开发出一种新的方法来迭代换能器。这种新方法建立在早期工作的基础上，但利用了许多新的概念和算法思想，通常在实验的帮助下诱导，这使其具有广泛的范围以及良好的性能。
2008-09-12 cs.LO
Quantitative Model Checking of Linear-Time Properties Based on Generalized Possibility Measures
基于可能性测度的线性时间特性的模型检验在以前的工作（Y。Li和L. Li，模型检验基于可能性度量的线性时间特性，IEEE Transactions on Fuzzy Systems，21（5）（2013），842-854）。然而，在以前的工作中考虑的线性时间性质是经典的和定性的，系统的可能性信息没有考虑在所有。本文将研究基于广义可能性测度的模糊线性时间性质的定量模型检验。使用可能性信息来描述系统的模型以及系统需要遵守的属性，以识别模型/属性中的不确定性。系统采用{ \sl广义可能性Kripke结构}（GPKS，简称）建模，其性质用模糊线性时间性质描述.具体地，研究了GPKS系统的可达性、总是可达性、约束可达性、重复可达性和持续性的模糊线性时间性质。介绍了GPKS中的模糊正则安全性质和模糊$ω-$正则性质，深入研究了模糊有限自动机对模糊正则安全性质和模糊$ω-$正则性质的验证.证明了有限GPKS中模糊正则安全性和模糊$ω-$正则性的验证可以转化为本文所介绍的产品GPKS中（总是）可达性和重复可达性（持久性）的验证.文中给出了几个算例来说明本文所提出的方法。
2016-01-25 cs.LO
Improving BDD Based Symbolic Model Checking with Isomorphism Exploiting Transition Relations
基于BDD的符号化模型检验大大提高了模型检验的适用性。然而，基于BDD的符号模型检验仍然非常消耗内存和时间。一个主要原因是系统之间复杂的过渡关系。有时，由于其穷举存储要求，甚至不可能生成转换关系。为了减少这个问题，已经提出了使用分区的过渡关系。然而，仍然有一些系统根本无法验证。此外，如果分区的粒度太细，则验证所需的时间可能增加。在本文中，我们的目标是异步并发系统的符号验证。对于这样的系统，我们提出了一种方法，它使用的相似性的过渡关系，以获得进一步的内存减少和运行时的改善。通过应用我们的方法，即使是以前棘手的过渡关系的系统的验证变得可行。
2011-06-07 cs.LO
Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability
研究了可达性关系上的多元模态逻辑的模型检验的计算复杂性和可满足性问题。首先，我们证明了所得到的逻辑的模型检验问题的组合复杂性是PTime完全的。其次，我们证明了可及性关系上的否定扩展的多元模态逻辑的可满足性问题是ExpTime-完全的。最后，我们证明了可达性关系上的置换和布尔运算符的多元模态逻辑的可满足性问题是ExpTime-完全的，在必要的假设下，可以使用的可达性关系的数量是有界的常数。
2022-10-03 cs.LO
Model-checking parametric lock-sharing systems against regular constraints
本文研究参数化锁共享系统在强公平性下的无限行为验证问题，证明其在嵌套锁使用下可判定且为 Exptime 完全，并在 spawn 参数有界时对固定秩奇偶自动机性质给出 Ptime 算法。
2023-07-10 cs.DC cs.FL cs.LO
Infinite State Model Checking by Learning Transitive Relations
RWTH Aachen University（亚琛工业大学）
通过学习传递关系，该方法扩展无限状态系统以证明安全性，结合递归分析与投影发现析取关系，并在LoAT工具中展现出强大的竞争力。
2026-02-02 cs.LO
Regular Model Checking Upside-Down: An Invariant-Based Approach
本文提出一种从上方逼近可达配置集合的常规模型检测补充方法，利用归纳不变量的交集构造正则自动机，并分析其复杂度与所需子句数。
2025-01-13 cs.DC cs.LO
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
HornStr 是首个将正则模型检验的不变式合成转化为字符串上的约束 Horn 子句问题的求解器，支持 L* 和基于 SAT 的自动机学习，并自动验证 MU 谜题，生成超 30000 个新基准。
2025-05-23 cs.FL cs.LO
On the Complexity of Verifying Regular Properties on Flat Counter Systems
在计数器系统验证的近似方法中，其中之一是模型检验其平坦展开。不幸的是，除了可达性查询或过去的LTL模型检查问题的复杂性表征，这种业务模型并不总是很好地研究。在本文中，我们描述的复杂性的模型检测问题的平面计数器系统的规约语言，包括一阶逻辑，线性μ演算，无限自动机，和相关的形式主义。我们的研究结果跨越不同的复杂性类（主要是从PTime到PSpace），它们适用于计数器值的算术约束系统允许的语言。就证明技术而言，我们提供了一种集中于主要问题的统一方法。
2013-04-23 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
Efficient Symmetry Reduction and the Use of State Symmetries for Symbolic Model Checking
一种减少时态逻辑模型检验中状态空间爆炸问题的技术是对称性约简。由于轨道关系的BDD过大，使得使用BDD的对称性约简和符号模型检验的组合长期受到影响。动态对称约化动态地计算状态的等价类的代表，从而避免了轨道关系的构造。本文提出了一种基于动态对称约简的高效模型检验算法。我们的实验表明，该算法是非常快的，并允许验证较大的系统。我们还实现了使用状态对称性进行符号对称性约简。据我们所知，我们是第一个结合基于BDD的符号模型检验研究状态对称性的人。
2010-06-08 cs.LO
Model Checking Temporal Properties of Recursive Probabilistic Programs
本文研究了递归概率程序（pPDA）针对 $ω$-可见下推语言的模型检测问题，给出了可判定性与复杂性结果，证明 CaRet 等逻辑可指定过程调用与返回匹配等结构化性质。
2023-12-14 cs.FL cs.LO
Nested Words for Order-2 Pushdown Systems
研究了2阶可折叠的高阶下推系统（CPDS）对带有push/pop匹配关系的MSO和PDL（propositional dynamic logic with converse and loop）的线性时间模型检验.为了捕捉这些线性时间行为与匹配，我们提出了2阶嵌套的话。这些图由一个词结构与两个二进制匹配关系，一个堆栈的每一个顺序，这与相应的堆栈上的匹配弹出（或折叠）推增强。由于匹配关系，可满足性和模型检验是不可判定的。因此，我们提出了一个欠近似，限制1阶推送可以弹出的次数。利用这种下近似，它仍然允许无限的堆栈高度，我们得到的可满足性和模型检验的MSO和PDL的可判定性。问题是PDL的ExpTime-Complete。
2016-09-20 cs.FL cs.LO
Learning to Prove Safety over Parameterised Concurrent Systems (Full Version)
我们重新审视了经典的问题，证明安全的参数化并发系统，即，用有限（符号）方法表示的有限状态并发系统的无限族。这样的无限族的一个例子是一个用餐哲学家协议，具有任意数量的n个进程（n是定义无限族的参数）。常规模型检验是一种用于参数化并发系统建模的通用框架，其中无限组的配置（分别为：transitions）由正则集（resp.常规换能器）。虽然在常规的模型检验框架中验证安全属性通常是不可判定的，但是在过去的15年中已经开发了许多复杂的半算法，可以在许多实际情况中成功地证明安全性。在本文中，我们提出了一个简单的解决方案，利用Angluin的经典L* 算法（及其变体）来合成正则归纳不变量。我们提供了一个终止保证时，从一组给定的初始配置可达的配置集是定期的。我们已经测试了L* 算法的标准（以及新的）的例子，在定期的模型检验，包括用餐哲学家协议，用餐密码协议，和几个互斥协议（如面包店，伯恩斯，Szymanski，和德国）。我们的实验表明，尽管我们的解决方案的简单性，它可以执行至少以及现有的半算法。
2017-10-03 cs.FL cs.LO cs.PL
Functional Reduction to Speed Up Bounded Model Checking
Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
FRAIG-BMC通过功能简化减少冗余，提升边界模型检查的效率和性能。
2025-12-07 cs.LO
Optimal Stateless Model Checking under the Release-Acquire Semantics
我们提出了一个框架，有效地应用无状态模型检验（SMC）的并发程序下运行的释放-获取（RA）片段的C/C++11内存模型。我们的方法是基于探索可能的程序顺序，它定义了线程的指令被执行的顺序，和读取关系，它指定如何读取从写入获得它们的值。这与先前的方法相反，先前的方法也探索可能的相干顺序，即，冲突写入之间的排序。由于意外的测试结果，如程序崩溃或断言违规只依赖于从关系的读取，我们避免了潜在的重要来源的冗余。我们的框架是基于一种新的技术，用于确定是否一个特定的读取关系是可行的RA语义下。我们定义了一个SMC算法，这是可证明的最佳意义上说，它探讨了每个程序的顺序和读取从关系正好一次。这个最优性结果是严格强于以前类似的最优性结果，这也考虑到相干顺序。我们已经在工具Tracer中实现了我们的框架。实验表明，Tracer可以显着快于国家的最先进的工具，可以处理RA语义。
2018-09-10 cs.FL cs.LO cs.PL
Model Checking Constraint LTL over Trees
约束自动机是Büchi自动机的一种改进，它处理来自某种关系结构S的数据字。这样一个自动机的每一个转换都带有S的关系的约束。只有当当前和下一个数据值满足转换的所有约束时，才能触发转换。这些自动机已被用于设置，其中S是一个线性顺序，以确定约束LTL的约束S。在本文中，S是无限分枝的无限阶树T。给出了T-约束自动机空性的PSPACE算法。这一结果暗示了T上约束LTL的可满足性和模型检验问题的PSPACE完备性。
2015-04-23 cs.LO
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
Model-Checking for Successor-Invariant First-Order Formulas on Graph Classes of Bounded Expansion
本文证明在后继不变一阶公式的模型检测问题上，当底层 Gaifman 图类具有有界扩张时该问题是固定参数可解的，从而推广了此前关于平面图、排除固定子式等图类的结果。
2017-05-21 cs.LO
Bounded Model Checking of Temporal Formulas with Alloy
Alloy是一种基于一阶关系逻辑的形式化建模语言，它不支持指定反应式系统。我们建议使用时序逻辑来指定这样的系统，并显示如何有界模型检验可以与合金分析仪进行。
2015-06-25 cs.LO cs.SE
Subsumption Checking in Conjunctive Coalgebraic Fixpoint Logics
虽然在扩展完整布尔基的逻辑中进行推理是困难的，但限制于模态语言的合取片段有时允许即使在存在最大不动点的情况下也进行易于处理的推理。一个这样的例子是EL家族的描述逻辑;在这里，有效的推理是基于满意度检查在适当的小模型，表征公式的模拟。然而，众所周知，并不是每一种合取模态语言都有一个易于处理的推理问题。自然的问题是，这些易处理的片段有多常见，以及如何识别它们。在这项工作中，我们提供了足够的条件，在一般的方式，考虑未标记的Tableau规则，为一个给定的模态逻辑的易处理性。我们工作的框架内的coalgebraic逻辑作为一个统一的语义设置。除了恢复已知的结果描述逻辑，如EL和FL 0，我们获得了新的关联和非关联模态逻辑的最大不动点的合取片段。最值得注意的是，我们发现了游戏逻辑和交替时间μ演算的易处理片段。
2014-06-06 cs.LO
Forward Analysis and Model Checking for Trace Bounded WSTS
我们研究了良结构变迁系统（WSTS）的一个子类，即Ginsburg和Spanier（trans. AMS 1964）意义下的有界完全确定性系统，我们认为它为Finkel和Goubault-Larrecq（Logic. Meth. Comput. Sci. 2012年）。事实上，我们证明，不同于其他条件考虑以前终止的前向分析，有界性是可判定的。有界性被证明是一个有价值的限制WSTS验证，因为我们表明，它进一步允许决定所有的$ω$ -经常属性的无限的痕迹的系统。
2016-03-04 cs.LO
Multi-Objective Model Checking of Markov Decision Processes
研究并给出了马尔可夫决策过程多目标模型检验问题的有效算法。给定MDP，M，以及给定多个线性时间（ω-正则或LTL）性质φ i，以及概率ri ε[0，1]，i=1，.，k，我们问是否存在控制器的策略σ，使得对于所有i，由σ控制的M的轨迹满足φ i的概率至少为ri。我们提供了一个算法，决定是否存在这样的策略，如果是这样产生它，并运行在时间多项式中的MDP的大小。这种策略可能需要同时使用随机化和内存。我们还考虑了更一般的多目标ω-正则查询，我们激励与应用的假设保证组合推理的概率系统。注意，在不同属性之间可以存在折衷：以高概率满足属性φ 1可能需要以低概率满足φ 2。将其视为多目标优化问题，我们需要关于“权衡曲线”或帕累托曲线的信息，以最大化不同属性的概率。我们证明了在MDP的大小下，可以计算关于时间多项式中的一组ω-正则性质的近似Pareto曲线。我们的定量上限使用LP方法。我们还研究了定性的多目标模型检验问题，我们表明，这些可以通过纯粹的图论方法进行分析，即使策略可能仍然需要随机化和内存。
2008-11-11 cs.CC cs.GT cs.LO
Parity Game Reductions
奇偶博弈在模型检验和可满足性检验中起着核心作用。求解奇偶性博弈在计算上是昂贵的，除其他外，由于博弈的大小，对于模型检验问题，其可以容易地包含$10^9$顶点或更多。等价关系可以用来减少奇偶博弈的规模，从而潜在地减轻部分计算负担。我们重新考虑（治理）互模拟和（治理）口吃互模拟，我们给出了详细的证明，这些关系是等价的，有唯一的等价物，他们近似的获胜地区的奇偶游戏。此外，我们提出了基于游戏的这些关系的特征。使用这些特征，我们的等价关系的奇偶游戏，可以在文献中找到，如直接模拟等价和延迟模拟等价。为了完成概述，我们开发的直接和延迟模拟等价的共归纳特征，我们建立了一个等价的奇偶游戏格。
2016-03-21 cs.GT cs.LO
Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes
针对马尔可夫决策过程中多目标ω-正则查询，提出独立可验证的证书与证据，扩展改进现有证书推导MILPs找最小见证子系统，特例下用无歧义Büchi自动机获单指数空间算法，实现并验证技术有效性。
2025-08-25 cs.LO
Trees over Infinite Structures and Path Logics with Synchronization
我们提供了无限树结构的模型检测问题的可判定性和不可判定性的结果。这些树结构由无限关系结构的元素序列构建。更准确地说，我们处理的关系结构M的树迭代在Shelah-Stupp的意义。与经典的MSO逻辑模型检验可判定的结果相反，我们证明了只允许路径量词和链量词的逻辑树模型检验问题的可判定性（其中链是路径的子集），因为它们出现在分支时间逻辑中;然而，同时树被等层关系丰富（如果顶点u、v在相同的树层上，则在顶点u、v之间保持）。我们将树逻辑与用于表达底层结构M的属性的逻辑干净地分离。我们说明的范围内的可判定性的结果表明，两个轻微的扩展框架导致不可判定性。特别地，这适用于Muchnik-Walukiewicz意义上的（更强的）树迭代。
2011-11-14 cs.LO
Model checking strategy-controlled systems in rewriting logic
本文针对 Maude 内置 LTL 模型检测器无法验证策略控制规约的问题，提出策略感知扩展，并结合表达力分析、应用示例和性能比较验证其有效性。
2024-01-15 cs.LO
Model-checking positive equality free logic on a fixed structure (direttissima)
本文为以模型为参数的正无等词逻辑模型检测问题的四类复杂度分类提供了仅基于关系的新直接证明，并开发了新算法解决无限结构中NP和co-NP成员资格问题。
2024-08-25 cs.LO
