Strategies, model checking and branching-time properties in Maude
| Autor: | Rubén Rubio, Isabel Pita, Narciso Martí-Oliet, Alberto Verdejo |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Model checking
Logic Computer science Programming language Extension (predicate logic) computer.software_genre Theoretical Computer Science Branching (linguistics) Nondeterministic algorithm TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Strategy language Resource (project management) Computational Theory and Mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Rewriting computer Software |
| Zdroj: | Journal of Logical and Algebraic Methods in Programming. 123:100700 |
| ISSN: | 2352-2208 |
| DOI: | 10.1016/j.jlamp.2021.100700 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect