Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strategies, model checking and branching-time properties in Maude

Rubén Rubio, Narciso Martí-Oliet, Isabel Pita, Alberto Verdejo

TL;DR

This work extends Maude by enabling branching-time model checking for strategy-controlled systems. It builds on prior LTL support by introducing a small-step operational semantics for the Maude strategy language and defining finite, bisimilar Kripke structures to verify $CTL^*$ and $μ$-calculus properties via external backends. The authors connect Maude models to backends such as LTSmin, NuSMV, Spot, and pymodelchecking through a unified umaudemc interface, enabling on-the-fly verification and visualization. The river-crossing and vending-machine examples illustrate how strategies shape execution trees and how model-checking results (including counterexamples) depend on the strategy; the approach is shown to be extensible and practically effective for a range of temporal logics. Overall, the paper demonstrates a modular, extensible verification pipeline that integrates strategy-controlled rewriting with established model-checking engines, aiding formal analysis of complex concurrent systems in Maude.

Abstract

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 $μ$-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.

Strategies, model checking and branching-time properties in Maude

TL;DR

This work extends Maude by enabling branching-time model checking for strategy-controlled systems. It builds on prior LTL support by introducing a small-step operational semantics for the Maude strategy language and defining finite, bisimilar Kripke structures to verify and -calculus properties via external backends. The authors connect Maude models to backends such as LTSmin, NuSMV, Spot, and pymodelchecking through a unified umaudemc interface, enabling on-the-fly verification and visualization. The river-crossing and vending-machine examples illustrate how strategies shape execution trees and how model-checking results (including counterexamples) depend on the strategy; the approach is shown to be extensible and practically effective for a range of temporal logics. Overall, the paper demonstrates a modular, extensible verification pipeline that integrates strategy-controlled rewriting with established model-checking engines, aiding formal analysis of complex concurrent systems in Maude.

Abstract

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 -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.
Paper Structure (27 sections, 19 theorems, 15 equations, 6 figures, 1 table)

This paper contains 27 sections, 19 theorems, 15 equations, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Comparison with the workshop paper
  3. Structure of the paper
  4. Preliminaries
  5. Strategies and transition systems
  6. Strategies
  7. Execution trees
  8. Rewriting logic
  9. The Maude strategy language
  10. Model checking
  11. Model checking strategy-controlled systems
  12. Generalization of two logics for strategy-controlled systems
  13. CTL*
  14. $\mu$-calculus
  15. Specification and model checking in Maude by an example
  16. ...and 12 more sections

Key Result

Theorem 1

Given an intensional strategy $\lambda$, there is a finite Kripke structure $\mathcal{K}'$ bisimilar to $\mathcal{U}(\mathcal{K}, \lambda)$ if $E(\lambda)$ is $\omega$-regular. The converse does not hold, but in that case $\ell(E(\lambda))$ is $\omega$-regular.

Figures (6)

  • Figure 1: Partial rewriting tree for the river-crossing puzzle.
  • Figure 2: Structure of the strategy model-checker modules.
  • Figure 3: Model graph for the safe strategy.
  • Figure 4: Strategy rewrite graph for $\alpha$ and $\beta$.
  • Figure 5: Architecture of the umaudemc model-checking tool.
  • ...and 1 more figures

Theorems & Definitions (33)

  • Definition 1
  • Definition 2: fscd
  • Definition 3: unwinding
  • Definition 4
  • Theorem 1
  • Proposition 1
  • Proposition 2
  • Proposition 3: principmc
  • Proposition 4: handbookmc
  • Proposition 5
  • ...and 23 more