Compositionality, Decompositionality and Refinement in Input/Output Conformance Testing - Technical Report
我们提出了一个输入/输出一致性测试理论，利用模态接口自动机与输入拒绝（IR-MIA）作为新的行为形式主义的规范和测试下的实现。IR-MIA上的模态细化关系允许区分强制性和允许的输出行为，以及隐式未指定和显式禁止的输入行为。因此，该理论支持积极和消极的一致性测试与乐观和悲观的环境假设。我们进一步表明，由此产生的一致性关系IR-MIA，称为模态irioco，享有许多理想的属性有关组件为基础的行为。首先，模态-irioco在模态加细下被保留，并在一定的限制下构成一个预序，这可以通过IR-MIA的规范输入完成来确保。其次，在相同的限制下，模态-irioco相对于具有多播和隐藏的IR-MIA的并行合成是合成的。最后，IR-MIA上的商运算符，作为并行组合的逆，有助于一致性测试中的分解，以解决未知组件的问题。
2019-02-14 cs.FL cs.LO cs.SE
On the Compositionality of Quantitative Information Flow
本文研究定量信息流中$g$-泄露的组合性，针对可分解信道系统，推导出整体$g$-泄露的界限，并推广了最小熵泄露和并行信道的结果。
2017-08-14 cs.IT cs.LO math.IT
Compositionality of Lyapunov functions via assume-guarantee reasoning
University of Strathclyde（斯特拉斯克莱德大学）；Topos Institute（托波斯研究所）
本文提出一个范畴框架，用于安全问题的假设-保证推理，通过将系统视为镜头，为参数化微分方程系统特别适应了假设-保证推理，特别是针对局部输入到状态稳定性（L）ISS李雅普诺夫函数。
2026-04-03 cs.LO math.CT math.DS
Composing Codensity Bisimulations
本文利用代数与余代数层面的余密度提升，将分配律提升问题归结为余密度提升间的分配律构造，并给出简化充分条件，用于证明自动机等状态系统行为等价性及行为度量的组合性。
2024-05-22 cs.LO math.CT
Structural operational semantics for non-deterministic processes with quantitative aspects
一般框架最近已被提出作为过程的统一理论结合非确定性与定量方面（如概率或随机定时执行），旨在提供一般的结果和工具。本文在这方面提供了两个贡献。首先，我们提出了一个通用的GSOS规范格式和相应的概念互模拟的非确定性过程的定量方面。这些规范根据ULTraS模型定义了带标签的转换系统，ULTraS模型是通常的LTS的扩展，其中转换关系将任何源状态和转换标签与状态可达性权重函数（例如，概率分布）。该格式因此被称为权重函数GSOS（WF-GSOS），覆盖许多已知系统及其互模拟（例如PEPA、TIPP、PCSP）和GSOS格式（例如GSOS、加权GSOS、Segala-GSOS等）。第二个贡献是这些系统作为一类函子的余代数的特征，参数的重量结构。这一结果使我们能够证明的WF-GSOS规范格式的合理性和完整性，这些规范所引起的双相似性总是同余。
2015-06-30 cs.LO
Contract-based Design and Verification of Multi-Agent Systems with Quantitative Temporal Requirements
本文提出定量假设-保证契约，实现多智能体系统在定量时间逻辑LTL[$\mathcal{F}$]规范下的组合式设计与验证，提高可扩展性和模块化。
2024-12-17 cs.LO
Weighted Modal Transition Systems
规格说明理论作为一种模型驱动的基于构件的软件系统开发过程的工具，近年来引起了人们的广泛关注。然而，目前的规范理论本质上是定性的，因此在某种意义上是脆弱的，即模型对系统的不可避免的近似，加上硬件平台的基本不可预测性，使得很难将基于模型的行为结论转移到实际系统。因此，这种方法可以说不适合现代软件系统。我们在这里提出的第一个规格理论，它允许捕捉定量方面的改进和实施过程中，从而利用定性设置的问题。我们提出的定量规范框架使用加权模态转换系统作为规范的正式模型。这些被标记为具有附加特征的转换系统，它们可以对系统可能实现或可能不实现的可选行为进行建模。通过引入加权模态转换系统之间距离的概念，将满意度和精细化从众所周知的定性提升到我们的定量设置。我们表明，定量版本的平行组成，以及商（对偶平行组成）继承的布尔设置的属性。
2012-10-20 cs.LO
Maximum Realizability for Linear Temporal Logic Specifications
基于线性时序逻辑（LTL）规范的自动综合广泛应用于机器人运动规划、自治系统控制和电网负荷分配等领域。在这样的应用程序中，一个常见的规范模式包括一个LTL公式，描述了对系统的行为的要求，以及一组额外的理想属性。我们研究的综合问题的整体规格是无法实现的设置，更准确地说，当一些理想的属性必须（暂时）违反，以满足系统的目标。我们提供了一个定量的语义集的安全规范，并使用它来正式的“尽力而为”的满足这样的软规范，同时满足硬LTL规范。我们提出了一种算法，用于合成的实现，是最佳的定量语义。我们的方法建立在有界合成方法的思想，我们开发了一个MaxSAT编码，允许最大限度地满足安全规范的定量。我们评估我们的算法从机器人和配电网络的情况。
2018-04-02 cs.LO cs.SE
Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives
我们展示了如何自动构建一个系统，满足给定的逻辑规范，并具有最佳的平均行为与比率成本的规范。当从一个逻辑规范合成一个系统时，经常会有几个不同的系统满足这个规范。在这种情况下，用户通常不容易正式声明她喜欢哪个系统。先前的工作提出通过在规范中添加定量方面来对正确的系统进行排名。期望的偏好关系可以用（i）定量语言来表达，定量语言是为系统的每个可能行为分配值的函数，以及（ii）定义系统的期望的优化标准的环境模型，例如，最坏情况或平均最优情况。在本文中，我们展示了如何合成一个系统，是最佳的（i）定量语言给出的自动机与比率成本函数，和（ii）环境模型给出的标记马尔可夫决策过程。该系统的目标是最小化预期（比率）成本。该解决方案是基于减少马尔可夫决策过程的比率成本函数，不需要在分母的成本是严格的积极的。我们找到一个最佳的策略，这些使用分数线性规划。
2011-02-21 cs.LO
Better Quality in Synthesis through Quantitative Objectives
大多数规约语言只表达定性约束。然而，在满足给定规范的两个实现中，一个可能优于另一个。例如，如果一个规范要求每个请求后面都有一个响应，那么人们可能更喜欢快速生成响应但不生成不必要的响应的实现。我们使用定量属性来衡量一个实现的“好”。使用具有相应量化目标的游戏，我们可以合成“最佳”实现，这是满足给定规范的可能实现集合中的首选。特别是，我们展示了如何自动机与字典的平均支付条件可以用来表达许多有趣的定量反应系统的属性。在这个框架中，最佳实现的合成需要解决的字典的平均回报游戏（安全要求），和解决的游戏与字典的平均回报和奇偶性的目标（活性要求）。我们提出了解决这两种新型图游戏的算法。
2013-05-28 cs.GT cs.LO
GSOS for non-deterministic processes with quantitative aspects
最近，一些通用框架已被提出作为统一的理论，结合非确定性与定量方面（如概率或随机定时执行）的过程，旨在提供一般的结果和工具。本文在这方面提供了两个贡献。首先，我们提出了一个通用的GSOS规范格式（和相应的互模拟概念）的非确定性过程的定量方面。这些规范根据ULTraS模型定义了带标签的转换系统，ULTraS模型是通常的LTS的扩展，其中转换关系将任何源状态和转换标签与状态可达性权重函数（例如，概率分布）。该格式因此被称为权重函数SOS（WFSOS），覆盖许多已知系统及其互模拟（例如PEPA、TIPP、PCSP）和GSOS格式（例如GSOS、加权GSOS、Segala-GSOS等）。第二个贡献是这些系统作为一类函子的余代数的特征，参数的重量结构。这一结果使我们能够证明的WFSOS规范格式的合理性，这些规范引起的双相似性总是同余。
2014-06-09 cs.LO cs.PL
A Robust Specification Theory for Modal Event-Clock Automata
在最近的一系列工作中，我们已经介绍了一个通用的定量推理规范理论的框架。本文的贡献是展示如何将这个框架可以应用于产生一个强大的规范理论的时间规格。
2012-07-18 cs.FL cs.LO
TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments
我们提出了暴风雨，一个合成工具，自动创建正确的建设反应系统和屏蔽定性或定量的规格在概率环境中。屏蔽是一种特殊类型的用于运行时实施的反应式系统;即，屏蔽件强制执行运行系统的给定定性或定量规范，同时尽可能少地干扰其操作。执行定性或定量规范的屏蔽分别称为安全屏蔽或最优屏蔽。安全防护罩可以作为预防护罩或后防护罩来实现，最佳防护罩作为后防护罩来实现。预屏蔽放置在系统之前，并限制系统的选择。后屏蔽在系统之后实现，并且能够覆盖系统的输出。Tempest是基于概率模型检查Storm，增加了模型检验算法，用于安全和平均回报目标的随机游戏。据我们所知，Tempest是唯一一个能够解决2-1/2玩家游戏的合成工具，具有平均收益目标，而不受状态空间的限制。此外，Tempest还增加了合成安全和最佳策略的功能，这些策略实现了反应式系统和护盾
2021-05-26 cs.LO
Semiring-based Specification Approaches for Quantitative Security
我们的目标是提供不同的半环为基础的正式工具的规格的安全要求：我们定量地提高了开放系统的方法，根据该系统是部分指定的。因此，我们假设存在一个未知的，可能是恶意的代理，与系统并行交互。两个规范框架沿着两条不同（但仍然相关）的路线设计。首先，通过比较一个系统的行为与预期的，或通过检查这样的系统是否满足一些安全要求：我们研究了一种新的近似行为等价比较进程的行为，从而扩展了广义非演绎成分（GNDC）的方法与分数。作为第二个结果，我们配备了一个模态逻辑与半环值的目的有一个权重相关的满足公式，指定一些要求的属性。最后，我们概括了经典的部分模型检查功能，我们将其命名为定量部分模型检查，以这种方式指出系统必须满足的必要和充分条件，以便被认为是安全的，相对于一个固定的安全/功能阈值。
2015-09-29 cs.CR cs.FL cs.LO
Categorical semantics of compositional reinforcement learning
LTCI, Télécom Paris, Institut Polytechnique de Paris（巴黎电信学院、巴黎电信、巴黎理工学院）；The University of Iowa（爱荷华大学）；The University of Texas at Austin（德克萨斯大学奥斯汀分校）
本文提出基于范畴论的组合强化学习框架，通过MDP范畴的推出操作实现任务组合，并统一安全与对称性概念。
2025-09-07 cs.AI cs.LO cs.SY
Quantitative Supermartingale Certificates
本文提出一种使用超鞅证书进行定量模型检查与控制综合的通用方法，通过随机不变量界定时间平移不变规约的满足概率，并提供了首个计算ω-正则与线性时序逻辑规约满足概率上下界的超鞅证书。
2025-04-07 cs.LO cs.SY eess.SY
Refining Timing Uncertainty from Logical Time Specification to Operation
Inria（法国国家信息与自动化研究所）；Université Côte d'Azur（蔚蓝海岸大学）
本文提出基于CCSL的细化时序规范框架，分三层次引入时序知识，将随机信息作为细化附加，支持增量集成，并在OCaml工具及软件定义车辆用例中验证。
2026-09-16 cs.LO
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
研究了并发系统对提示线性时态逻辑（Prompt Linear Temporal Logic，LTL）规范的满足情况。LTL是LTL的一个扩展，它允许指定可能性满足的参数界限，从而为规约语言增加了一个定量方面。我们建立了有界公平性，有界口吃等价性，和满足的LTL \X公式之间的连接。基于这种连接，我们证明了不同类别的系统与参数数量的组件和定量规格的第一截止结果，从而确定以前未知的可判定片段的参数化模型检验问题。
2019-11-15 cs.FL cs.LO
Symbolic BDD and ADD Algorithms for Energy Games
能源游戏，模拟有限资源的定量消耗，例如，时间或能量，在反应系统的定量模型中起着核心作用。反应合成构造满足给定规格的控制器，如果存在的话。对于能量博弈，一个综合控制器不仅保证满足安全约束的规范，而且还表示在能量博弈的定量约束。最近由Chatterjee等人提出的能量博弈的符号算法，它在数量值的表示上是象征性的，但在游戏状态和过渡的表示上是具体的。在本文中，我们提出了一个算法，这是象征性的定量值和基本的游戏表示。我们已经实现了我们的算法使用两种不同的符号表示反应式游戏，二元决策图（BDD）和代数决策图（ADD）。我们调查的共性和差异的两个实现，并比较他们的运行时间的能源游戏的规格。
2016-11-23 cs.DS cs.GT cs.LO
Expressive Temporal Specifications for Reward Monitoring
本文提出基于定量线性时间逻辑的奖励监控方法，用于提升强化学习中奖励密度和训练效率。
2025-12-29 cs.AI cs.LG cs.LO
Formal Modelling and Analysis of Slot Machines
针对老虎机行为复杂、玩家影响下RTP难确定的问题，提出用概率过程规范建模老虎机行为、非确定性建模玩家干预，将RTP表述为可自动求值的量化模态公式，在真实老虎机上验证了方法，实现精确RTP计算与最优玩家策略获取。
2024-07-09 cs.LO
Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis
在布尔合成中，我们给出了一个LTL规范，目标是构建一个转换器，在对抗环境中实现它。通常，一个规范既包含对抗性环境下应该满足的布尔需求，也包含多值组件，这些组件指的是满足的质量，并且我们希望在概率环境下最小化其预期成本。在这项工作中，我们研究，第一次，平均支付游戏中，系统的目标是在概率环境中的预期成本最小化，同时肯定满足$ω$ -经常性条件对抗的环境。我们考虑的情况下，$ω$ -正则条件是作为一个奇偶目标或由LTL公式。我们表明，在一般情况下，最优策略不需要存在，而且，极限值不能近似的有限记忆策略。因此，我们专注于计算的极限值，并给出严密的复杂性界合成$ε$ -最优策略的有限内存和无限内存的战略。我们表明，我们的游戏自然出现在各种情况下的合成与布尔和多值目标。除了直接应用之外，在与某些行为的成本和回报的合成中，它允许我们计算$ω$的最小感测成本-常规规格-一种质量度量，其中我们寻找最小化从输入读取的预期信号数量的传感器。
2016-04-24 cs.FL cs.LO
Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods
Stanford University（斯坦福大学）；Toyota Research Institute（丰田研究院）
提出了一种利用计算图计算信号时序逻辑（STL）公式的定量语义的方法，称为STLCG。STLCG提供了一个平台，使逻辑规范纳入机器人问题，受益于基于梯度的解决方案。具体来说，STL是一种功能强大、表达能力强的形式化语言，它可以指定连续系统和混杂系统产生的信号的空间和时间属性。STL的定量语义提供了一个鲁棒性度量，即，信号满足或违反STL规范的程度。在这项工作中，我们设计了一个系统的方法来翻译STL的鲁棒性公式到计算图。通过这种表示，并利用现成的自动微分工具，我们能够有效地通过STL鲁棒性公式进行反向传播，从而实现STL规范与机器人技术中使用的许多基于梯度的方法的自然和易于使用的集成。通过一些来自各种机器人应用的例子，我们证明了STLCG是通用的，计算效率高，并能够将人类领域的知识到问题的制定。
2021-12-27 cs.CL cs.LO cs.SY
Quantitative Monitoring of Signal First-Order Logic
Zeroth Research（零次研究）；Institute of Science and Technology Austria（奥地利科学技术研究所）；CISPA Helmholtz Center for Information Security（CISPA赫尔姆霍兹信息安全中心）；Leiden University（莱顿大学）
本文提出了一种基于鲁棒性的SFO定量语义，实现了对信号一阶逻辑的高效在线监测，并展示了其在实时属性评估中的有效性。
2026-03-03 cs.LO cs.SE cs.SY
Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation
在许多合成问题中，生成不仅满足功能约束而且随机化以提高多样性、鲁棒性或不可预测性的实现是至关重要的。最近提出的控制即兴（CI）的框架提供了技术的正确的建设合成的随机系统受到硬和软的约束。然而，以前的CI工作主要集中在定性规范上，而在机器人规划和其他领域，我们通常有定量的质量指标，可以相互交易。例如，巡逻安全机器人的设计者可能想知道平均巡逻时间需要增加多少，以确保机器人路线的特定方面足够多样化，因此不可预测。在本文中，我们使这种类型的应用程序，通过推广CI问题，以支持定量软约束约束的预期值的一个给定的成本函数，和随机性约束，强制执行多样性的生成的痕迹相对于一个给定的标签功能。我们建立了标记的定量CI问题的基本理论，并开发了有效的算法来解决这些问题时，规格编码的有限自动机。我们还提供了一个近似的即兴算法的基础上约束求解任何规格编码为布尔公式。我们证明了我们的问题制定和算法的实用性与实验应用它们来产生不同的机器人规划问题的近最优计划。
2022-06-06 cs.FL cs.LO cs.SY
