arXiv 1604.065032016-04cs.LO

行为规范理论的线性时间分支时间谱

A Linear-Time Branching-Time Spectrum for Behavioral Specification Theories

Uli Fahrenberg, Axel Legay

摘要：

我们提出了行为规范理论的线性时间-分支时间谱中的大多数等价物。几乎所有以前的工作规范理论的重点是双相似性，但有一个明确的兴趣规范理论的其他前序和等价。我们表明，规范理论的前序不能存在和发展的一般计划，使我们能够定义行为规范理论的基础上，析取模态转换系统，大多数等价的线性时间-分支时间谱。

英文摘要：

We propose behavioral specification theories for most equivalences in the linear-time--branching-time spectrum. Almost all previous work on specification theories focuses on bisimilarity, but there is a clear interest in specification theories for other preorders and equivalences. We show that specification theories for preorders cannot exist and develop a general scheme which allows us to define behavioral specification theories, based on disjunctive modal transition systems, for most equivalences in the linear-time--branching-time spectrum.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

行为规范理论：一个代数分类学

Behavioral Specification Theories: an Algebraic Taxonomy

我们开发了一个不同的行为规范理论的分类，并揭示其代数属性。我们首先澄清什么恰恰构成了行为规范理论，然后介绍逻辑和结构操作，并开发由此产生的代数属性。为了激励我们的发展，我们给出了大量的例子，不同的操作行为规范理论。

2020-09-23cs.LO

具有规则行为规范的霍尔逻辑

A Hoare Logic with Regular Behavioral Specifications

我们提出了一个霍尔逻辑，扩展程序规范与正则表达式，捕获的行为在执行过程中出现的事件序列。这个想法类似于会话类型或类流程行为契约，这是两个目前流行的研究方向。这里提出的方法在表现力和证明自动化之间取得了特定的平衡，值得注意的是，它可以在多次循环迭代中捕获有趣的顺序行为。该方法是模块化的，并与自动演绎验证工具集成良好。我们描述和演示我们的原型实现SecC使用两个案例研究：匹配的电子邮件地址和规范的游戏步骤中的VerifyThis赌场的挑战。

2022-05-13cs.FLcs.LO

行为程序逻辑和无延续的LAGC语义（技术报告）

Behavioral Program Logic and LAGC Semantics without Continuations (Technical Report)

我们提出的行为程序逻辑（BPL），跟踪属性的动态逻辑，结合了行为类型的概念，并允许推理的非功能性的属性内的一个微积分。BPL使用行为模式[s|- τ ]，以针对行为规范τ验证语句s。行为规范概括了后置条件和行为类型。它们可用于指定其他静态分析，例如，数据流分析这使得对同一程序的多个分析结果的演绎推理成为可能，可能以不同的形式实现。我们的演算BPL验证的行为规范逐渐，常见的行为类型。这极大地简化了局部结果的规范、演算和组成。我们提出了一个面向对象的演员与期货，集成了指针分析和桥梁之间的差距行为类型和演绎验证的微积分。本技术报告介绍了（1）没有延续的核心活动对象语言（CAO）的完整LAGC语义（2）行为程序逻辑和（3）给出了行为程序逻辑中表示的行为类型的示例，方法类型。此报告包含方法类型的可靠性证明。虽然语义覆盖了带有挂起的CAO，但方法类型没有，以简化表示。

2019-04-30cs.LOcs.PL

GeneSyst：一个推理B事件规范行为方面的工具。适用于安全属性。

GeneSyst: a Tool to Reason about Behavioral Aspects of B Event Specifications. Application to Security Properties.

在本文中，我们提出了一种方法和工具，以建立符号标记的B规格转换系统。这个名为GeneSyst的工具可以考虑细化级别，并可以可视化抽象状态在具体层次状态中的分解。由此产生的符号转换系统代表了初始B事件系统的所有行为。因此，它可以用来推理它们。我们说明了使用GeneSyst检查电子钱包模型的安全属性。

2010-04-09cs.CRcs.LO

一次判定所有行为等价：用于线性时间-分支时间谱系的光谱游戏

Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy

本文提出一种广义双模拟游戏，用于从线性时间-分支时间谱系中自动寻找区分有限状态过程的Hennessy-Milner逻辑公式，并确定过程间最粗的行为等价关系。

2022-08-08cs.FLcs.GTcs.LO

相干分支特征互模拟

Coherent branching feature bisimulation

在软件产品线的行为分析在家庭水平的进展受益于进一步发展的基本语义理论。在这里，我们提出了一个行为等价的特征转换系统（FTS）广义分支互模拟标记的转换系统（LTS）。我们证明了分支功能互模拟的一个家庭的产品的FTS与分支互模拟的LTS投影的每个单独的产品。对于相干分支特征互模拟的一个限制性概念，我们进一步提出了一个极小化算法，并证明了它的正确性。虽然相干分支特征互模拟的最小化问题被证明是棘手的，在一个小的案例研究结果的设置中的算法的应用程序在一个显着的加速模型检验的行为属性。

2015-04-14cs.LOcs.SE

更多相关论文收起更多论文

概率转移系统的根分支互模拟同余

Rooted branching bisimulation as a congruence for probabilistic transition systems

我们提出了一个概率转换系统规范格式，被称为概率RBB安全，根分支互模拟是一个同余。同余定理是基于Fokkink的定性情况下的方法。要做到这一点，需要扩展标记转换系统设置中的转换系统规范理论，以处理句法和语义上的概率分布。我们提供了一个无干扰的表征的概率分支互模拟适应Andova等人的工作。交替模型。给出反例来证明格式所需的各种条件。

2015-09-29cs.LO

线性时间分支过程的模型检验

Linear-Time Model Checking Branching Processes

（多类型）分支过程是生成随机无限树的自然和充分研究的模型。分支过程具有非确定性和概率性分支，推广了转移系统和马尔可夫链（但不是一般的马尔可夫决策过程）。我们研究了模型检验分支过程对线性时间ω-正则规范的复杂性：它是几乎肯定的情况下，由分支过程随机生成的树的每个分支满足ω-正则规范？主要结果是，对于LTL规格这个问题是在PSPACE，包含经典的结果，分别为过渡系统和马尔可夫链。底层的一般模型检查算法是基于自动机理论的方法，使用明确的Büchi自动机。

2021-07-04cs.FLcs.LO

分支时间时序逻辑范式的表达能力

On the Expressive Power of the Normal Form for Branching-Time Temporal Logics

随着涉及复杂分布式系统的新兴应用，分支时间规范特别重要，因为它们反映了此类应用的动态和非确定性。我们描述了一个简单而强大的分支时间规范框架的表达能力-分支时间范式（BNF），它已被开发为分支时间时序逻辑的子句解析的一部分。我们显示的编码的布奇树自动机的语言的范式，从而表示，语法，树自动机在一个高层次的方式。因此，我们可以把BNF作为后者的范式。这些结果使我们能够（1）将给定的问题规格转换为范式，并作为一种验证方法的演绎推理技术-小句的时间分辨率;（2）适用于解决方法的核心组成部分之一-循环搜索提取，句法，隐藏的不变量在广泛的复杂的时间规格。

2022-04-14cs.FLcs.LO

非确定性概率模型的分歧分析

Analyzing Divergence for Nondeterministic Probabilistic Models

本文系统比较了非确定性概率系统中细化分支和弱概率互模拟的分歧敏感行为等价关系，并给出了这些等价关系的高效检验算法。

2024-12-28cs.LO

端点充分性行为商

Endpoint Sufficiency Behavioral Quotients

该研究针对带来源标注的生成系统，提出三种端点充分性层次，建立严格层次关系，给出计算精确分支商的划分精化过程，为保留来源提供仅区分行为差异的准则。

2026-08-10cs.LO

余代数行为度量

Coalgebraic Behavioral Metrics

该研究在余代数框架下提出两种推广Kantorovich和Wasserstein伪度量的函子提升方法，推导状态行为伪度量，并给出提升分配律与单子的充分条件以建模线性时间度量，拓展了行为度量的理论范畴。

2024-07-15cs.LO

Maude中的策略、模型检验与分支时间性质

Strategies, model checking and branching-time properties in Maude

本文扩展Maude模型检验能力，使其支持策略控制系统上的CTL*和μ-演算分支时间性质验证，并通过通用高效连接集成外部模型检验器并比较其性能。

2024-01-15cs.LO

分支互模拟与弱迹语义之间谱系的单一能量博弈

One Energy Game for the Spectrum between Branching Bisimilarity and Weak Trace Semantics

本文首次用单一多维能量博弈统一刻画并判定带静默步的线性时间—分支时间谱系中从分支互模拟到弱迹等价的行为等价，并通过 Hennessy–Milner 逻辑的八个表达力维度建立正确性。

2024-11-21cs.LO

分支双相似性的Upto技术

Up-to Techniques for Branching Bisimilarity

自从引入过程的行为等价以来，人们一直在寻找伴随这些等价的有效证明技术。强双相似性和弱双相似性都伴随着一系列最新的技术：它们的证明方法的增强。对于分支双相似性，这些结果尚未建立。我们表明，一个强大的证明技术是健全的分支双相似性相结合的三种技术，最多工会，最多的扩展和布卢姆的BB酷格式的背景。然后，我们提出了一个初步的建议铸造的正确性证明的上下文技术在一个抽象的coalgebraic设置，包括分支，但也η，延迟和弱双相似。

2020-01-24cs.LO

考虑静默步骤的线性时间-分支时间谱分析

Linear-Time--Branching-Time Spectroscopy Accounting for Silent Steps

该研究首次给出带静默步骤的van Glabbeek线性时间-分支时间谱的广义博弈刻画，用多维能量博弈一次性刻画判定多类弱行为等价，并结合Hennessy-Milner逻辑的八维表达力证明其正确性。

2024-10-07cs.GTcs.LO

智能环境中情境感知应用的行为识别和分析

Behavior recognition and analysis in smart environments for context-aware applications

在情景感知和主动性至关重要的普适计算中，提供有关智能环境中行为的准确/适当信息是一项具有挑战性和关键性的任务。行为标识使得能够抽象出应用程序感兴趣的更高级别的概念。这项工作提出了统一的基于逻辑的框架来识别和分析行为规范理解为一个形式逻辑语言，避免歧义典型的自然语言。从感知数据流中自动发现行为作为形式化规范对于构建无缝的人机交互具有重要意义。因此，有关环境行为的知识表示的时间逻辑公式构成了一个基础的反应性和精确的推理过程，以支持可信的，明确的和主动的决策，智能和上下文感知的应用程序。

2016-01-20cs.LO

分支时间时序逻辑的自动机理论刻画

Automata-Theoretic Characterisations of Branching-Time Temporal Logics

本文通过识别Hesitant Tree Automata的两个变体，为任意分支树上的CTL*和ECTL*等分支时间时序逻辑提供了自动机理论刻画，解决了悬而未决四十年的开放问题。

2024-04-29cs.LO

分支位置互模拟等价

Branching Place Bisimilarity

本文将位置互模拟扩展到带静默动作的有限Petri网，提出分支位置互模拟$\approx_p$及其较粗变体$\approx_d$，证明二者均可判定，并证明$\approx_d$严格细于分支全并发互模拟。

2023-09-23cs.LO

在Move中对命令式一等函数的形式验证

Formal Verification of Imperative First-Class Functions in Move

Aptos Labs（Aptos实验室）

本文研究了Move语言中命令式一等函数的形式验证，通过引入行为谓词和状态标签，实现了对函数值的高效表示与验证，支持Rust风格的引用和全局变量修改，并提升了SMT编码效率。

2026-08-14cs.LOcs.PLcs.SE

分支时间逻辑的可满足性对策

Satisfiability Games for Branching-Time Logics

分支时间时态逻辑如CTL*、CTL和CTL+的可满足性问题在程序规范和验证中有重要的应用。它们的计算复杂性是已知的：CTL* 和CTL+对于双指数时间是完全的，CTL对于单指数时间是完全的.这些逻辑的一些决策程序是已知的;它们使用树自动机，tableaux或公理系统。在本文中，我们提出了一个统一的博弈论框架，这些分支时间时序逻辑的可满足性问题。我们定义可满足性游戏的完整的分支时间时序逻辑CTL* 使用高层次的定义获胜的条件，抓住了最少不动点展开的本质的良好基础。这些获胜条件构成了ω-词的形式语言。我们分析了在何种情况下需要哪种确定性ω-自动机来识别这些语言。然后，我们得到一个减少的问题，解决奇偶校验或Büchi游戏。所获得的算法的最坏情况下的复杂性匹配这些逻辑的已知下界。这种方法提供了一个统一的，但复杂性理论上的最佳处理分支时间时序逻辑的可满足性。它将时序逻辑机器的使用与自动机的使用分开，从而保留了输入公式和表示可满足性的对象之间的语法关系，即奇偶或Büchi游戏中的获胜策略。这里介绍的游戏只在输入公式的Fischer-Ladner闭包上工作。最后但并非最不重要的是，这里提出的游戏来尝试提供工具支持复杂的分支时间逻辑，如CTL* 和CTL+的可满足性问题。

2013-10-15cs.LO

计算树逻辑中的性质推断

Inferring Properties in Computation Tree Logic

针对分支时间逻辑规范推断研究不足的问题，提出一种基于反例引导的算法，通过生成不可取模型从有限状态模型中推断出简洁且语言极小的CTL公式，并首次开发了基于SAT编码的被动学习算法。

2023-10-20cs.FLcs.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-28cs.FLcs.LO