Confluence of Equational Generalized Term Rewriting Systems with Application to Rewrite Theories and Maude
Equational Generalized Term Rewriting Systems (EGTRSs) extend Equational Term Rewriting Systems by considering replacement restrictions on selected arguments of function symbols, as in Context-Sensitive Rewriting, and conditional equations and rewriting rules whose conditional part may include not only a mix of the usual (reachability, joinability,...) conditions, but also atoms defined by a set of Horn clauses. This tutorial explains how to prove and disprove confluence (modulo) of EGTRSs by using appropriate finite sets of conditional pairs. Our results apply to well-known classes of rewriting-based systems. In particular, to Equational (Conditional) Term Rewriting Systems and Conditional Rewrite Theories, which provides a formal basis to describe computations in Maude.
Author: Salvador Lucas
Statistical Model Checking with QMaude
QMaude is a framework for describing probabilistic models and other quantitative aspects on top of nondeterministic specifications in the highly-expressive language Maude, based on rewriting logic. These models can be analyzed by probabilistic and statistical model-checking methods using the umaudemc tool. In this tutorial, we focus on statistical model checking, explain its theoretical background, explain several recently added features extending the statistical model checking capabilities of QMaude, show how to use the tool, and illustrate its applications with several examples.