Name
Abstract | ||
|---|---|---|
This paper proposes the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature. We start by defining a modal action logic (VLRL) in which rewrite rules are captured as actions. The main novelty of this logic is a topological modality associated with state constructors that allows us to reason about the structure of states, stating that the current state can be decomposed into regions satisfying certain properties. Then, on top of the modal logic, we define a temporal logic for reasoning about properties of the computations generated from rewrite theories, and demonstrate its potential by means of several examples. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1093/logcom/exi015 | J. Log. Comput. |
Keywords | Field | DocType |
state constructor,verification logic,modal logic,temporal logic,topological modality,main novelty,certain property,modal action logic,global manner,rewriting logic,different modal,current state | Discrete mathematics,Computational logic,Algorithm,Substructural logic,Multimodal logic,Linear temporal logic,Theoretical computer science,Philosophy of logic,Predicate logic,Dynamic logic (modal logic),Mathematics,Higher-order logic | Journal |
Volume | Issue | ISSN |
15 | 3 | 0955-792X |
Citations | PageRank | References |
6 | 0.46 | 0 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Narciso Martí-oliet | 1 | 1357 | 97.35 |
| Isabel Pita | 2 | 47 | 8.27 |
| José Luiz Fiadeiro | 3 | 1567 | 186.97 |
| José Meseguer | 4 | 9533 | 805.39 |
| Tom Maibaum | 5 | 281 | 31.90 |