In previous work, summarized in this paper, we proposed an operation of parallel composition for rewriting-logic theories, allowing compositional specification of systems and reusability of components. The present paper focuses on compositional verification. We show how the assume/guarantee technique can be transposed to our setting, by giving appropriate definitions of satisfaction based on transition structures and path semantics. We also show that simulation and equational abstraction can be done componentwise. Appropriate concepts of fairness and deadlock for our composition operation are discussed, as they affect satisfaction of temporal formulas. We keep in parallel a distributed and a global view of composed systems. We show that these views are equivalent and interchangeable, which may help our intuition and also has practical uses as, for example, it allows global-style verification of a modularly specified system.

翻译：在之前的工作（本文已总结）中，我们提出了一种针对重写逻辑理论的并行组合操作，支持系统的组合式规范与组件的可重用性。本文聚焦于组合验证。我们展示了如何通过基于迁移结构与路径语义的适当满足定义，将假设/保证技术移植到我们的框架中。同时证明模拟与等式抽象可以按组件方式实现。针对组合操作讨论了公平性与死锁的适当概念，因为这些概念会影响时态公式的满足性。我们并行保持了组合系统的分布式视图与全局视图，并证明这两种视图等价且可互换——这不仅有助于直观理解，也具有实际用途，例如允许对模块化规范的系统进行全局式验证。