TY - GEN

T1 - Towards a verification logic for rewriting logic

AU - Fiadeiro, José Luis

AU - Maibaum, Tom

AU - Martí-Oliet, Narciso

AU - Meseguer, Jose

AU - Pita, Isabel

N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2000.

PY - 2000

Y1 - 2000

N2 - This paper is an initial step in 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 two simple examples.

AB - This paper is an initial step in 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 two simple examples.

UR - http://www.scopus.com/inward/record.url?scp=84947265907&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84947265907&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-44616-3_25

DO - 10.1007/978-3-540-44616-3_25

M3 - Conference contribution

AN - SCOPUS:84947265907

SN - 3540678980

SN - 9783540678984

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 438

EP - 458

BT - Recent Trends in Algebraic Development Techniques - 14th International Workshop, WADT 1999, Selected Papers

A2 - Bert, Didier

A2 - Choppy, Christine

A2 - Mosses, Peter

PB - Springer

T2 - 14th International Workshop on Algebraic Development Techniques, WADT 1999

Y2 - 15 September 1999 through 18 September 1999

ER -