Rewriting logic and its implementation Maude are an expressive framework for the formal specification and verification of software and other kinds of systems. Concurrency is naturally represented by nondeterministic local transformations produced by the application of rewriting rules over algebraic terms in an equational theory. Some aspects of the global behavior of the systems or additional constraints sometimes require restricting this nondeterminism. Rewriting strategies are used as a higher-level and modular resource to cleanly capture these requirements, which can be easily expressed in Maude with an integrated strategy language. However, strategy-aware specifications cannot be verified with the builtin LTL model checker, making strategies less useful and attractive. In this paper, we discuss model checking for strategy-controlled systems, and present a strategy-aware extension of the Maude LTL model checker. The expressivity of the strategy language is discussed in relation to model checking, the model checker is illustrated with multiple application examples, and its performance is compared.

翻译：重写逻辑及其实现Maude是用于软件及其他系统形式化规约与验证的表达性框架。并发性可通过等式理论中代数项上应用重写规则所产生的非确定性局部变换自然地表示。系统全局行为的某些方面或附加约束有时需要限制这种非确定性。重写策略作为一种高层且模块化的资源，能够简洁地捕获这些需求，并通过Maude集成的策略语言轻松表达。然而，策略感知的规约无法使用内置的LTL模型检验器进行验证，这使得策略的实用性与吸引力大打折扣。本文讨论了策略控制系统的模型检验问题，并提出了一种策略感知的Maude LTL模型检验器扩展。本文结合模型检验探讨了策略语言的表达性，通过多个应用实例演示了模型检验器，并对其性能进行了比较分析。