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
Branching-Time Model Checking Gap-Order Constraint Systems (Extended Version)
研究了带间隙序约束系统的模型检验问题。分支时间时序逻辑CTL，特别是它的片段EG和EF。GCS是由整数值变量的演化描述的非确定性无限分支过程，服从形式为$x-y\ge k$的Presburger约束，其中$x$和$y$是变量或常数，$k\in\mathbb{N}$是非负常数。我们表明，EG模型检验是不可判定的GCS，而EF是可判定的。特别是，这意味着GCS和有限状态系统之间的强和弱互模拟等价的可判定性。
2015-02-25 cs.LO
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 Constraint LTL over Trees
约束自动机是Büchi自动机的一种改进，它处理来自某种关系结构S的数据字。这样一个自动机的每一个转换都带有S的关系的约束。只有当当前和下一个数据值满足转换的所有约束时，才能触发转换。这些自动机已被用于设置，其中S是一个线性顺序，以确定约束LTL的约束S。在本文中，S是无限分枝的无限阶树T。给出了T-约束自动机空性的PSPACE算法。这一结果暗示了T上约束LTL的可满足性和模型检验问题的PSPACE完备性。
2015-04-23 cs.LO
Typestate Checking and Regular Graph Constraints
我们引入了正则图约束，并探讨其可判定性。规则图约束的动机是1）在存在链接的数据结构的情况下改变对象类型的类型检查，2）形状分析技术，以及3）在树和网格上的类似约束的泛化。我们定义了一个称为堆的图子类，作为程序在执行过程中构造的数据结构的抽象。证明了堆类上正则图约束蕴涵的有效性是不可判定的。我们表现出不可判定性表现出一定的“对应图”的存在和不存在的同态有限数量的固定图的特征。正则图约束蕴涵的不可判定性意味着，当这些属性用任何规约语言表达时，都没有算法来验证过程前提条件是否满足，或者不变量是否保持不变，至少与正则图约束一样具有表达性。
2004-08-05 cs.LO cs.PL
Symbolic model checking of tense logics on rational Kripke models
本文引入了有理Kripke模型类，研究了基本时态逻辑Kt的符号模型检验及其在该类模型中的一些扩展。有理Kripke模型基于（通常是无限的）有理图，顶点由某些正则语言中的单词标记，转换由异步双头有限自动机（也称为有理转换器）识别。在理性Kripke模型中，每个原子命题都在一组规则的状态中求值。证明了Kt的每个公式在每个有理Kripke模型中都有一个有效的可计算正则扩张，从而证明了有理Kripke模型中Kt的局部模型检验和全局模型检验是可判定的.这些结果被提升到Kt的一些扩展。我们研究并部分确定了模型检验过程的复杂性。
2008-10-30 cs.LO
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
Checking Behavioral Consistency Constraints for Pervasive Context in Asynchronous Environments
上下文一致性检查是上下文感知应用中必不可少的一部分，它是对上下文属性的特定约束的检查。为了描述和适应普适计算环境中的动态变化，上下文感知应用程序通常需要指定和检查上下文上的行为一致性约束。这个问题是具有挑战性的，主要是由于分布式和异步的普适计算环境的性质。具体而言，检查行为约束的关键问题是上下文活动的时间顺序。上下文活动通常涉及多个上下文收集设备，这些设备是完全分散的并且以异步方式交互。然而，现有的上下文一致性检查方案不工作在异步环境中，因为它们隐含地假设一个全局时钟的可用性或中继同步的交互。为此，我们提出了有序的全球活动（OGA）算法，它检测的基础上谓词检测在异步环境中的全球活动的顺序。我们的方法的本质是消息的因果关系和它的动态编码为异步环境中的逻辑向量时钟。我们实现了在异步环境中的谓词检测的中间件基础设施（MIPA），OGA算法的实现和评估。评估结果表明，行为一致性约束检查的影响，这证明了我们的工作的主要动机。实验结果还表明，OGA可以在动态普适计算环境中实现行为一致性约束的精确检测。
2009-11-01 cs.LO cs.SE
Constraint LTL Satisfiability Checking without Automata
本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。
2014-02-11 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
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
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
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
在以前的工作中，第一作者扩展到高阶重写和依赖类型中使用类型中的大小注释，这是一种终止证明技术，称为基于类型或大小的终止，最初为ML类程序开发。在这里，我们通过考虑条件重写和显式量化以及对大小注释的约束更进一步。这允许更精确地描述函数输出的大小如何取决于其输入的大小。因此，我们可以检查更多函数的终止。首先给出了一个基于约束求解的通用类型检测算法。然后，我们给出了Presburger算法中的一个带约束的终止准则。据我们所知，这是高阶条件重写的第一个终止准则，考虑到终止的条件。
2006-09-11 cs.LO
Regular Model Checking Upside-Down: An Invariant-Based Approach
本文提出一种从上方逼近可达配置集合的常规模型检测补充方法，利用归纳不变量的交集构造正则自动机，并分析其复杂度与所需子句数。
2025-01-13 cs.DC cs.LO
Model-checking parametric lock-sharing systems against regular constraints
本文研究参数化锁共享系统在强公平性下的无限行为验证问题，证明其在嵌套锁使用下可判定且为 Exptime 完全，并在 spawn 参数有界时对固定秩奇偶自动机性质给出 Ptime 算法。
2023-07-10 cs.DC cs.FL cs.LO
Constraint-Based Deadlock Checking of High-Level Specifications
在形式化方法的许多应用中，确定没有死锁是很重要的。模型检验用于发现形式化模型中的死锁的使用通常是有限的。在本文中，我们提出了一个基于约束的方法来寻找死锁采用ProB约束求解器。我们提出的一般技术，以及各种改进，必须进行ProB的Prolog内核，如具体化的成员资格和算术约束。这项工作是由一个工业案例研究指导的，博世的一个团队正在对巡航控制系统进行建模。在这个案例研究中，ProB能够快速找到非常大的无死锁约束的反例。在本文中，我们还介绍了这种新技术的其他成功应用。使用SAT和SMT求解器对这些约束的实验迄今为止是不成功的。
2011-09-09 cs.LO cs.PL cs.SE
Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
本文通过为{log}语言定义类型系统并实现类型检查器，将类型检查与集合约束求解结合，提高了软件验证的自动化程度，并通过两个工业案例验证了其有效性。
2024-03-21 cs.LO cs.PL
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
Constraint-Driven Modeling Enabling Dual Model Checking and Simulation for Discrete Event Systems
Arizona State University（亚利桑那州立大学）
本文提出Constraint-DEVS方法，扩展DEVS-Suite框架以支持离散事件系统的仿真与模型检查，开发并验证了片上网络模型，为该框架的混合引擎提供了设计制品。
2026-08-25 cs.AR cs.LO cs.SE
On the Complexity of Verifying Regular Properties on Flat Counter Systems
在计数器系统验证的近似方法中，其中之一是模型检验其平坦展开。不幸的是，除了可达性查询或过去的LTL模型检查问题的复杂性表征，这种业务模型并不总是很好地研究。在本文中，我们描述的复杂性的模型检测问题的平面计数器系统的规约语言，包括一阶逻辑，线性μ演算，无限自动机，和相关的形式主义。我们的研究结果跨越不同的复杂性类（主要是从PTime到PSpace），它们适用于计数器值的算术约束系统允许的语言。就证明技术而言，我们提供了一种集中于主要问题的统一方法。
2013-04-23 cs.LO
Automatic Verification of Timed Concurrent Constraint Programs
时间并发约束（Timed Concurrent Constraint，tccp）是并发约束编程（Concurrent Constraint Programming，cc）范式的扩展，它允许我们指定时间至关重要的并发系统，例如反应式系统。可以有无限多个状态的系统可以在tccp中指定。模型检验是一种能够自动验证具有大量状态的有限状态系统的技术。在过去的几年里，一些研究已经调查了如何扩展模型检验技术的系统具有无限数量的状态。在本文中，我们提出了一种方法，利用tccp的计算模型。基于约束的计算允许我们定义一种方法，将模型检验算法应用于（一类）无限状态系统。我们扩展的经典算法的模型检验LTL的一个特定的逻辑定义的验证tccp和tccp结构，我们在这项工作中定义的建模程序的行为。我们定义了一个限制的时间，以得到一个有限的模型，然后我们开发了一些说明性的例子。据我们所知，这是第一个为tccp定义模型检验方法的方法。
2005-05-11 cs.LO
Traversing automata with current state uncertainty under LTL$_f$ constraints
本文研究路径上的LTL$_f$模型检测问题，识别出多项式空间可解的一般条件，并针对零件定向问题中的特定约束给出PSPACE完全和NP完全情形，同时证明同步性约束不改变复杂度。
2023-11-29 cs.FL cs.LO
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
在基于服务的应用程序的执行过程中出现的一个重要问题涉及确定是否可以用具有不同接口的服务来替换正在运行的服务的能力，例如，如果前者不再可用。标准有界模型检验技术可用于执行此检查，但它们必须能够非常快速地提供答案，以免检查妨碍应用程序的可操作性，而不是帮助它。当考虑会话服务时，问题变得更加复杂，即，服务，公开其中具有输入/输出数据依赖关系的操作。在本文中，我们介绍了一个形式化验证技术的线性时序逻辑，允许用户在公式中的整数变量的约束的扩展。这种技术适用于会话服务的可替代性问题被证明是相当快，比现有的内存占用更小。
2010-04-16 cs.LO cs.SE
Model Checking ofWorkflow Nets with Tables and Constraints
本文针对带表格工作流网可达图存在伪状态且只能分析健全性的不足，提出带表格与约束的工作流网 WFTC-net，并定义 DCTL 逻辑及基于状态可达图的模型检测算法和工具，实验验证了其有效性。
2023-06-27 cs.FL cs.LO
Model Checking Probabilistic Pushdown Automata
我们考虑概率下推自动机（pPDA）的模型检验问题和各种概率逻辑中可表达的属性。我们开始与属性，可以制定为一个广义的随机游走问题的实例。我们证明了定性和定量的模型检验这类性质和pPDA是可判定的。然后，我们证明了模型检验的定性片段的逻辑PCTL和pPDA也是可判定的。此外，我们开发了一个容错的模型检验算法的PCTL和无状态pPDA的子类。最后，我们考虑了一类ω-正则性质，并证明了pPDA的定性和定量模型检验都是可判定的。
2006-03-09 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
Counting Constraints in Flat Array Fragments
我们确定了一个片段的Presburger算法丰富的自由函数符号和基数约束的解释集，这是适合自动化分析。我们建立这样一个片段的可判定性和复杂性的结果，我们实现我们的算法。在履行来自不变式检查和有界模型检查基准测试的证明义务的实验表明，我们的决策过程的实际可行性。
2016-02-01 cs.LO
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
Dynamic Consistency Checking in Goal-Directed Answer Set Programming
在回答集编程中，当程序上的约束变得不可满足时，就会出现不一致。在本文中，我们介绍了一种技术，为我们的目标导向的方法计算答案集的动态一致性检查，只有那些被认为是相关的部分答案集的约束进行测试，允许不一致的知识库被成功地查询。然而，该算法保证，如果一个程序至少有一个一致的答案集，返回的任何部分答案集将是某个一致答案集的子集。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-05-14 cs.LO
Dichotomies and Duality in First-order Model Checking Problems
我们研究的复杂性的模型检验问题，固定的模型A，在一定的片段L的一阶逻辑。这些有时被称为L的表达式复杂性。我们得到各种复杂性分类定理，这些逻辑L的范围在模型A，在二分法猜想的约束满足问题的精神-这本身可以被看作是模型检验问题的存在合取正一阶逻辑。
2006-11-28 cs.CC cs.LO
Model Checking Temporal Properties of Recursive Probabilistic Programs
本文研究了递归概率程序（pPDA）针对 $ω$-可见下推语言的模型检测问题，给出了可判定性与复杂性结果，证明 CaRet 等逻辑可指定过程调用与返回匹配等结构化性质。
2023-12-14 cs.FL cs.LO
A Linear-Time Nominal $μ$-Calculus with Name Allocation
无限字母表语言的逻辑和自动机模型，如Freeze LTL和寄存器自动机，用于验证过程或带有数据的文档。它们与名义集上的形式主义密切相关，例如非确定性轨道有限自动机（NOFA），其中名称扮演数据的角色。在这种形式主义中的推理问题在计算上往往是困难的。名字绑定的名义自动机模型，如规则的非确定性名义自动机（RNAs）已被证明是计算上更容易处理。在本文中，我们介绍了一个线性时间不动点逻辑Bar-muTL有限字在一个无限的字母表，它的特点是完全否定和冻结量化通过名称绑定。我们通过对扩展的正则非确定性名义自动机的非平凡约简表明，尽管Bar-muTL允许无限制的非确定性和无限多的寄存器，但RNAs上的模型检验Bar-muTL和可满足性检验都具有基本的复杂性.例如，模型检验在2 ExpSpace中，更准确地说是在参数化的ExpSpace中，有效地将寄存器的数量作为参数。
2021-08-20 cs.FL cs.LO
On the complexity of the model checking problem
在过去的二十年里，一阶逻辑的各种片段的模型检验问题引起了人们的广泛关注：特别是对于原始正片段和正Horn片段，它们分别被称为约束满足问题和量化的约束满足问题。事实上，这两个片段是目前唯一没有已知复杂性分类的片段。所有其他的句法片段可以很容易地分类，无论是直接或使用Schaefer的二分法定理SAT和QSAT，除了积极平等自由片段。这个突出的片段也可以被分类，并享有四分法：根据模型，相应的模型检验问题是易于处理的，NP完全的，co-NP-complete或Pspace-complete。此外，复杂度下降总是见证了一个通用的解决算法，使用量词相对化。此外，它的复杂性的特点是代数手段：存在或不存在特定的满射超运算之间的那些保持模型的复杂性。
2012-10-25 cs.CC cs.LO
The Complexity of Satisfiability Checking for Symbolic Finite Automata
本文研究符号有限自动机的可满足性问题，通过将其分解为输入字符理论与接受单词索引的单子二阶理论，获得了该自动机类及其线性算术约束扩展的紧计算复杂度界限。
2023-06-30 cs.LO
Model Checking Positive Equality-free FO: Boolean Structures and Digraphs of Size Three
本文研究了正无等式一阶逻辑上固定结构A的模型检验问题--非一致量化约束满足问题QCSP（A）的自然推广.我们证明了这个问题的一个完整的复杂性分类时，A的范围超过1。布尔结构和2.）有向图的大小（小于或等于）3。前者表现为对数空间与P空间完全的二分法，后者表现为对数空间、NP完全、co-NP完全和P空间完全的四分性。
2008-08-05 cs.CC 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
Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 cs.FL cs.LO cs.PL
Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
Radboud University（拉德堡德大学）；Brno University of Technology（布尔诺理工大学）
针对有限MDP上带结构约束的鲁棒奖励最优策略计算难题，本文提出结合可满足性求解器与概率模型检查的合成框架，实验证明其可行且性能媲美现有最优方法。
2025-11-15 cs.AI 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
Path Checking for MTL and TPTL over Data Words
本文研究了数据词上MTL与TPTL的路径检查问题，依据寄存器数量和约束编码方式给出完整复杂度分析，证明MTL为P完全、TPTL为PSPACE完全，并得出单计数器机器模型检查的精确复杂度。
2017-09-01 cs.LO
Model Checking One-clock Priced Timed Automata
我们考虑定价模型（a.k.a.加权）时间自动机，它是时间自动机的扩展，具有位置和转换的成本信息，我们基于对模态具有成本约束的经典时态逻辑的扩展来研究该模型的各种模型检查问题。我们证明，在假设模型只有一个时钟，模型检查这类模型对逻辑WCTL，CTL成本约束的方式，是PSPACE完全的（虽然它已被证明是不可判定的，只要模型有三个时钟）。我们还证明了模型检查WMTL，具有成本约束模态的LTL，只有当模型中有一个时钟和一个秒表成本变量（即，其斜率位于{0，1}中）。
2008-06-20 cs.CC cs.GT cs.LO
Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic
本文提出了一种近似方法来验证计数器系统相对于线性时态逻辑的表达计数扩展中制定的属性。它可以表达，例如，通过对运行中的特定位置进行计数并施加算术约束，确保应答的数量永远不会超过对服务的请求的数量。所解决的问题是不可判定的，因此解决了平坦的下近似的系统。这提供了一个灵活的可调整的穷举和计算工作量之间的权衡，类似于有界模型检验。最近的技术和结果的平坦Kripke结构的模型检查频率特性的解除和构造一个参数化编码的（近似）问题的量化器免费Presburger算法。基于z3 SMT求解器的原型实现证明了基于RERS挑战赛问题的方法的有效性。
2019-01-17 cs.LO cs.SE
Really Natural Linear Indexed Type Checking
最近的工作已经表明了线性索引类型系统在执行复杂程序属性方面的强大功能。这些系统将线性类型与类型级索引语言相结合，允许更细粒度的分析。这类系统在隐复杂性和差分隐私等领域得到了广泛的应用。增强这种方法的表现力的一种自然方法是，按照依赖类型的精神，允许索引依赖于运行时信息。这种方法在DFuzz中使用，DFuzz是一种用于差分隐私的语言。DFuzz类型系统依赖于一种索引语言，它支持对常量和变量进行实数和自然数运算。此外，DFuzz使用子类型机制使类型更加灵活。线性、依赖性和子类型本身在执行类型检查或类型推断时都需要精细的处理;它们的组合大大增加了这一挑战，因为这些特性可以以非平凡的方式进行交互。本文研究了DFuzz的类型检测问题。我们展示了如何减少类型检查（一个简单的扩展）DFuzz约束解决一阶理论的自然和实数，虽然不可判定，通常可以在实践中处理的标准数值求解器。
2015-03-16 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
Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes
针对马尔可夫决策过程中多目标ω-正则查询，提出独立可验证的证书与证据，扩展改进现有证书推导MILPs找最小见证子系统，特例下用无歧义Büchi自动机获单指数空间算法，实现并验证技术有效性。
2025-08-25 cs.LO
Model checking strategy-controlled systems in rewriting logic
本文针对 Maude 内置 LTL 模型检测器无法验证策略控制规约的问题，提出策略感知扩展，并结合表达力分析、应用示例和性能比较验证其有效性。
2024-01-15 cs.LO
On Verifying Timed Hyperproperties
我们研究的可满足性和模型检测问题的时间超属性指定的HyperMTL，HyperLTL的时间扩展。根据是否允许在不同的跟踪中交错事件，可以为定时超属性定义两种可能的语义：异步和同步。虽然可满足性问题可以决定类似于HyperLTL的语义的选择，我们表明，模型检查问题，除非规格是替代自由，是不可判定的，即使在非常有限的时间限制是允许的。在积极的一面，我们表明，模型检验HyperMTL与量词交替是可能的，在一定条件下的同步语义，或当有一个固定的时间域的长度上的界限。
2018-12-25 cs.LO
Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking
在基于定点运算的处理器中实现数字滤波器会导致与有限字长相关的问题。特别地，在这样的滤波器中的信号的处理可以产生由在累加加法和乘法运算期间的量化和舍入效应引起的溢出和不想要的噪声。在本文中，我们描述了一种新的方法来验证数字滤波器使用现成的有界模型检查器称为ESBMC，它支持完整的C/C++，是基于可满足性模理论求解器。特别是，我们能够验证溢出的发生，极限环，和时间约束的基础上实现的离散时间模型在C。实验表明，该方法可以用来验证数字滤波器定点实现中的潜在问题，从而可以有效地发现现实的设计错误。
2013-07-23 cs.LO cs.SE
