Reachability of Communicating Timed Processes
我们研究的可达性问题的通信时间进程，在离散和密集的时间。我们的模型包括自动机与本地的时间限制通信无界FIFO通道。每个自动机只能访问其本地时钟集;所有时钟都以相同的速率进化。我们的主要贡献是一个完整的表征的可判定和不可判定的通信拓扑结构，离散和密集的时间。我们也得到了复杂性的结果，通过显示，通信时间的进程至少是硬的Petri网，在离散时间，我们也表现出等价的Petri网。我们的研究结果遵循相互拓扑保持时间自动机和（非定时）计数器自动机之间的减少。
2012-10-17 cs.LO
Symbolic Simulation-Checking of Dense-Time Systems
直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。
2006-10-13 cs.LO cs.SE
Behavioral Analysis of Timed Actors using Syntactic Slice Equivalence
University of Tehran（德黑兰大学）；IT University of Copenhagen（哥本哈根信息技术大学）；University of Oslo（奥斯陆大学）；Mälardalen University（马尔默达尔大学）；KTH（皇家理工学院）
本文提出一种针对Timed Rebeca的静态切片等价性分析，证明其蕴含弱定时互模拟，从而在行为不变时重用微型孪生体，显著降低验证成本。
2026-09-17 cs.LO cs.PL
Time-Darts: A Data Structure for Verification of Closed Timed Automata
符号数据结构在模型检验时系统中的应用已成为一个重要的研究课题，在一些成熟的验证工具中，差分边界矩阵（DBMs）仍然是首选的数据结构。相比之下，离散化提供了一个简单的选择，所有的操作都具有线性时间复杂度的时钟数，但有效的封闭系统的一大类。不幸的是，细粒度的离散化会导致状态空间爆炸。我们引入了一种新的数据结构，称为时间箭头的符号表示的状态空间的时间自动机。与完全离散化相比，单个时间镖允许表示任意大的状态集合，但是时间镖上的操作的时间复杂度在时钟数量上保持线性。我们证明了建议的可达性算法的正确性，并进行了几个实验，以比较性能的时间飞镖和完全离散化。主要结论是，在我们所有的实验中，时间镖方法优于完全离散化，它的规模显着更好的模型与较大的常数。
2012-11-27 cs.DS cs.LO
LTL Parameter Synthesis of Parametric Timed Automata
参数时间自动机的参数综合问题是不可判定的，即使是非常简单的可达性。在本文中，我们引入了参数估值的限制下，参数综合问题是可判定的LTL性能。所研究的有界整数参数综合问题可以使用所有可能的参数赋值的显式枚举来解决。我们提出了一种替代的符号区域为基础的方法，这个问题的结果在一个更快的计算。我们的技术扩展了基于自动机的LTL模型检验的时间自动机的方法的思想。为了证明我们的方法的有用性，我们提供了实验评估和比较我们的方法与显式枚举技术。
2016-03-04 cs.FL cs.LO
Checking Timed Bisimulation with Bounded Zone-History Graphs -- Technical Report
时间自动机（TA）是一个行之有效的形式化描述离散状态/连续时间行为的时间临界反应系统。关于基本分析问题的候选人的实现对规范进行比较，都给定为TA，它已被证明，定时跟踪等价是不可判定的，而定时互模拟等价是可判定的。相应的证明利用区域图，一个有限的，但通常非常占用空间的TA语义表征。因此，大多数实用的TA工具利用区域图，而不是符号和一般更有效的表示TA语义，自动化分析任务。然而，区域图只产生声音的分析任务的结果被简化为平原可达性问题，从而检查定时双相似性太不精确。在本文中，我们提出了有界区域历史图，一种新的表征TA语义促进可调的权衡精度和可扩展性之间的时间双相似性检查。据我们所知，我们的工具TimBrCheck是目前唯一可用的工具，用于有效地检查定时双相似性，甚至支持无声移动的非确定性TA。我们进一步提出了实验结果，从应用我们的工具收集的社区基准，提供洞察精度和效率之间的权衡，取决于绑定值。
2020-09-16 cs.FL cs.LO
Efficient Monitoring of Timed Properties
Aalborg University（奥尔堡大学）；Queens University（女王大学）
本文针对实时系统的定时性质，提出基于差分边界矩阵的高效符号在线监测算法，在工具 MoniTAal 中实现后可有效监测长轨迹上的性质。
2026-08-05 cs.FL cs.LO
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
带抑制弧的参数时间Petri网（PITPN）允许参数在触发范围内，从而支持时间系统的灵活性。本文提出并证明了PITPN的一种具体的和符号化的重写逻辑语义。我们将展示如何使用Maude结合SMT解决方案，为PITPN提供完善的正式分析。我们开发了一个新的通用折叠符号可达性的方法，终止时的参数状态类图的PITPN是有限的。我们解释了几乎所有的形式分析和参数合成支持的国家的最先进的PITPN工具Roméo可以在Maude与SMT。此外，我们还支持从参数化初始标记进行分析和参数合成，以及使用用户定义的执行策略进行完整的LTL模型检验和分析。在三个基准上的实验表明，我们的方法在许多情况下优于Roméo。
2023-03-15 cs.LO
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
2021-10-22 cs.LO cs.PL
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
我们首先提出了一个大字母表上的有限自动机的语言等价性检查算法。我们使用符号自动机，其中的过渡函数是competently表示使用（多端）二进制决策图（BDD）。其关键思想在于通过符号化地探索可达对来计算互模拟，从而避免冗余。这个想法可以结合现有的优化，我们特别显示了一个很好的集成与不相交集森林数据结构从Hopcroft和卡普的标准算法。然后，我们考虑Kleene代数与测试（KAT），代数理论，可用于验证从编译器优化到网络编程分析的各个领域。这个理论是可判定的减少到语言等价的自动机上的保护字符串，一种特殊的自动机，有指数大的字母。我们提出了几种方法，允许构造符号自动机的KAT表达式，根据Brzozowski的衍生物或标准的自动机结构。总而言之，这导致了用于确定KAT表达式的等价性的有效算法。
2014-07-09 cs.FL cs.LO
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Shanghai Jiao Tong University（上海交通大学）
提出Irene框架，通过保结构符号化简在门级、混合路径和及密度核三个层次验证混合量子程序等价性，在1982个程序对中解决79.92%，并发现15个编译器缺陷。
2026-09-30 cs.LO cs.PL cs.SE
A Reduced Semantics for Deciding Trace Equivalence
本文针对安全协议迹等价判定中的状态爆炸问题，提出精简符号语义，通过偏序归约消除冗余交错，并集成于工具 APTE，基准测试显示显著性能提升。
2017-06-07 cs.LO
Protocol Analysis with Time
我们提出了一个框架，适合于分析的密码协议，利用时间在其执行。我们提供了一个进程代数语法，使时间信息提供给进程，并考虑到时间的基本属性的转换语义。如果需要，用户可以添加其他属性。该定时协议框架可以实现为仿真工具或符号分析工具，其中时间参考由逻辑变量表示，并且其中时间的属性被实现为对这些时间逻辑变量的约束。这些约束是在协议的符号执行过程中执行的。这些约束的可满足性可以在分析过程中进行评估，因此违反物理定律的攻击可以被拒绝为不可能的。我们证明了我们的方法的可行性，通过使用Maude-NPA协议分析仪与SMT求解器，用于评估的可满足性的时间约束。我们提供了一个健全的和完整的协议转换，从我们的时间进程代数的Maude NPA的语法和语义，我们证明了它的健全性和完整性。然后，我们使用该工具来分析黑手党欺诈和距离劫持攻击的距离绑定协议套件。
2020-10-26 cs.CR cs.LO
Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems
VRAIN, Universitat Politècnica de València（瓦伦西亚理工大学）；LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord（索邦巴黎北大学）
研究实时系统形式分析中无穷性的两个维度，提出基于归约的验证方法，整合重写、归约及约束存储等技术，引入折叠机制确保终止，通过验证协议评估，能统一支持多种实时模型分析，为实时重写理论符号验证提供基础。
2026-07-24 cs.LO cs.PL cs.SC
A reduced semantics for deciding trace equivalence using constraint systems
安全协议的许多隐私类型的属性可以在适当的进程代数中使用迹等价属性来建模。已经表明，这样的性质可以确定为感兴趣的有限过程类（即，没有复制）。然而，这不足以获得实用工具。目前的原型遭受一个经典的组合爆炸问题所造成的许多交织的过程中的行为的探索。Mödersheim等人使用偏序约简技术解决了这个问题的可达性。我们重新审视他们的工作，推广它，并适应它的等价性检查。我们得到了一个优化的形式减少符号语义，消除了冗余的交织在飞行中。
2014-01-17 cs.CR cs.LO
Model-Checking Process Equivalences
过程等价是一种形式化的方法，它将程序和系统联系起来，这些程序和系统在非正式的情况下以相同的方式运行。由于没有唯一的概念，这意味着两个动态系统显示相同的行为有大量的形式过程等价，从互模拟跟踪等价，分类在线性时间分支时间谱。我们提出了一个逻辑框架的基础上表达模态不动点逻辑，它是能够定义许多过程等价关系：对于每个这样的等价有一个固定的公式，这是满足一对过程，当且仅当他们是等价的，就这个关系。我们解释了如何做模型检验，甚至象征性地，这个逻辑的一个重要片段，捕捉许多过程的等价。这允许将模型检验技术用于过程等价性检验。我们展示了如何部分评估可以用来获得决策程序的通用模型检验计划的过程等价。
2012-10-09 cs.LO
Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements
服务质量属性的保证是面向服务的软件工程的一个重要方面。所谓的服务级别协议（SLA）的表示法，例如Web服务级别协议（WSLA）语言，提供了正式的语法来指定服务提供商和客户之间的（具有法律约束力的）合同方面的此类保证。另一方面，用于验证概率实时的【形】行为的形式化方法已经达到了一定的表达能力和效率水平，可以将其应用于现实世界的场景中。本文建议采用最近引入的区间概率时间自动机（IPTA）模型来对面向服务系统的QoS属性进行形式化验证。具体来说，我们表明，IPTA与概率时间自动机（PTA）相比，能够直接捕获SLA中指定的保证。IPTA分析中的一个特殊挑战是，它们的朴素语义通常会产生无限的状态集和无限分支的转换。然而，使用符号表示，IPTA可以进行分析，而有效。我们已经开发了第一个实现的IPTA模型检查器扩展的PRISM工具，并表明，模型检验IPTA是只稍微贵于模型检验可比PTA。
2011-11-14 cs.LO cs.PF cs.SE
