Rewriting logic and its implementation Maude are a natural and expressive framework for the specification of concurrent systems and logics. Its nondeterministic local transformations are described by rewriting rules, which can be controlled at a higher level using a builtin strategy language added to Maude~3. This specification resource would not be of much interest without tools to analyze their models, so in a previous work, we extended the Maude LTL model checker to verify strategy-controlled systems. In this paper, CTL* and $\mu$-calculus are added to the repertoire of supported logics, after discussing which adaptations are needed for branching-time properties. The new extension relies on some external model checkers that are exposed the Maude models through general and efficient connections, profitable for future extensions and further applications. The performance of these model checkers is compared.

翻译：重写逻辑及其实现Maude是一种用于描述并发系统与逻辑的自然且富有表达力的框架。其非确定性局部变换由重写规则描述，并可通过Maude~3内置的策略语言在更高层次上加以控制。若无分析模型之工具，这一规约资源将意义有限，故而在前期工作中，我们扩展了Maude的LTL模型检验器以验证策略控制系统。本文在探讨分支时间性质所需适配项后，将CTL*与μ-演算纳入所支持的逻辑体系。该新扩展依托若干外部模型检验器，通过通用且高效的连接暴露Maude模型，为未来扩展与进一步应用奠定基础。比较了这些模型检验器的性能。