A Semantic Approach to the Analysis of Rewriting-Based Systems

TL;DR

This paper presents a semantic method for analyzing properties of rewriting-based systems, enabling the verification of complex system behaviors by model-theoretic techniques, often succeeding where traditional methods fail.

Contribution

It introduces a unified semantic approach to verify properties of rewriting systems, including infeasibility, non-joinability, and security aspects, surpassing existing specialized techniques.

Findings

Successfully analyzes infeasibility and non-joinability in rewriting systems

Applies to conditional rewriting and web security models

Outperforms traditional methods in certain cases

Abstract

Properties expressed as the provability of a first-order sentence can be disproved by just finding a model of the negation of the sentence. This fact, however, is meaningful in restricted cases only, depending on the shape of the sentence and the class of systems at stake. In this paper we show that a number of interesting properties of rewriting-based systems can be investigated in this way, including infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness of conditional rewrite systems, or the secure access to protected pages of a web site modeled as an order-sorted rewrite theory. Interestingly, this uniform, semantic approach succeeds when specific techniques developed to deal with the aforementioned problems fail.