Pacti：面向系统分析与设计的假设-保证推理规模化

Assume-Guarantee Abstraction Refinement for Probabilistic Systems

We describe an automated technique for assume-guarantee style checking of strong simulation between a system and a specification, both expressed as non-deterministic Labeled Probabilistic Transition Systems (LPTSes). We first characterize counterexamples to strong simulation as "stochastic" trees and show that simpler structures are insufficient. Then, we use these trees in an abstraction refinement algorithm that computes the assumptions for assume-guarantee reasoning as conservative LPTS abstractions of some of the system components. The abstractions are automatically refined based on tree c…

通过假设-保证推理实现李雅普诺夫函数的组合性

Compositionality of Lyapunov functions via assume-guarantee reasoning

本文提出一个范畴框架，用于安全问题的假设-保证推理，通过将系统视为镜头，为参数化微分方程系统特别适应了假设-保证推理，特别是针对局部输入到状态稳定性（L）ISS李雅普诺夫函数。

面向随机多智能体系统中能力的假设-保证验证

Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems

针对随机多智能体系统中策略能力模型检测的难题，本文提出带不完美信息的概率交替时间时序逻辑的假设-保证验证方案，证明其可靠性并讨论完备性，还提出捕获“最多达成φ”的非概率交替时间逻辑新变体。

Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information

Synthesis of program parts is very useful for concurrent systems. However, most synthesis approaches do not support common design tasks, like modifying a single process without having to re-synthesize or verify the whole system. Assume-guarantee synthesis (AGS) provides robustness against modifications of system parts, but thus far has been limited to the perfect information setting. This means that local variables cannot be hidden from other processes, which renders synthesis results cumbersome or even impossible to realize. We resolve this shortcoming by defining AGS in a partial information…

Assume-Guarantee Synthesis for Digital Contract Signing

We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents and the trusted third party (TTP) as path formulas in LTL and prove that the satisfaction of these objectives imply fairness; a property required of fair exchange protocols. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of assume-guarantee synthesis…

Monitoring Assumptions in Assume-Guarantee Contracts

Pre-deployment verification of software components with respect to behavioral specifications in the assume-guarantee form does not, in general, guarantee absence of errors at run time. This is because assumptions about the environment cannot be discharged until the environment is fixed. An intuitive approach is to complement pre-deployment verification of guarantees, up to the assumptions, with post-deployment monitoring of environment behavior to check that the assumptions are satisfied at run time. Such a monitor is typically implemented by instrumenting the application code of the component…

假设-保证契约代数是dp-代数

Assume-guarantee contract algebras are dp-algebras

本文为假设-保证契约规定了一组基本运算，从而将其代数结构刻画为众所周知的簇（dp-代数）的生成集合，解决了原构造缺乏明确基本运算的问题。

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability

The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizability is proven, is to construct such an implementation automatically, and thus solve the problem of program synthesis. In this paper, we propose a novel approach to pro- gram synthesis guided by k-inductive proofs of realizability of assume- guarantee contracts constructed from safety properties. The proof of re- alizability is performed over a set of forall-exists formulas, and synthesis is per- formed by extracting Sk…

通过假设-保证推理进行组合式归纳不变式推断

Compositional Inductive Invariant Inference via Assume-Guarantee Reasoning

本文提出一种基于假设-保证推理的组合式归纳不变式推断方法，通过将系统分解为组件并推断局部不变式，提高推断效率并提供模块化见解。

使用依赖保证规则推理并发循环和递归

Reasoning about concurrent loops and recursion with rely-guarantee rules

本文提出通用、机械验证的精化规则，用于在并发上下文中推理递归程序和while循环，采用依赖保证方法处理线程干扰，并基于不动点推导循环规则。

Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version)

We consider the problem of efficiently checking a set of safety properties P1,....,Pk of one design. We introduce a new approach called JA-verification where JA stands for "Just-Assume" (as opposed to "assume-guarantee"). In this approach, when proving property Pi, one assumes that every property Pj for j!=i holds. The process of proving properties either results in showing that P1,....,Pk hold without any assumptions or finding a "debugging set" of properties. The latter identifies a subset of failed properties that cause failure of other properties. The design behaviors that cause the proper…