Strategies, model checking and branching-time properties in Maude
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914642172837888 |
|---|---|
| author | Rubio, Rubén Martí-Oliet, Narciso Pita, Isabel Verdejo, Alberto |
| author_facet | Rubio, Rubén Martí-Oliet, Narciso Pita, Isabel Verdejo, Alberto |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_07680 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Strategies, model checking and branching-time properties in Maude Rubio, Rubén Martí-Oliet, Narciso Pita, Isabel Verdejo, Alberto Logic in Computer Science 68Q60 F.4.1; F.3.1 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. |
| title | Strategies, model checking and branching-time properties in Maude |
| topic | Logic in Computer Science 68Q60 F.4.1; F.3.1 |
| url | https://arxiv.org/abs/2401.07680 |