Critical systems require high reliability and are present in many domains. They are systems in which failure may result in financial damage or even loss of lives. Standard techniques of software engineering are not enough to ensure the absence of unacceptable failures and/or that critical requirements are fulfilled. Reo is a component-based modelling language that aims to provide a framework to build software based on existing pieces of software, which has been used in a wide variety of domains. Its formal semantics provides grounds to certify that systems based on Reo models satisfy specific requirements (i.e., absence of deadlocks). Current logical approaches for reasoning over Reo require the conversion of formal semantics into a logical framework. ReLo is a dynamic logic that naturally subsumes Reo's semantics. It provides a means to reason over Reo circuits. This work extends ReLo by introducing the iteration operator, and soundness and completeness proofs for its axiomatization.

翻译：关键系统需要高可靠性，并且存在于许多领域中。这些系统的故障可能导致经济损失，甚至人员伤亡。标准的软件工程技术不足以确保不存在不可接受的故障，也不足以确保关键需求得到满足。Reo是一种基于组件的建模语言，旨在提供一个基于现有软件组件构建软件的框架，已广泛应用于各种领域。其形式化语义为基于Reo模型的系统满足特定需求（例如，无死锁）提供了认证基础。当前用于推理Reo的逻辑方法需要将形式化语义转换为逻辑框架。ReLo是一种动态逻辑，能够自然地包含Reo的语义，并提供推理Reo电路的手段。本工作通过引入迭代算子扩展了ReLo，并给出了其公理化的可靠性和完备性证明。