@TechReport{LEHOG10-TR,
AUTHOR = {Lambers, Leen and Ehrig, Hartmut and Habel, Annegret and Orejas, Fernando and Golas, Ulrike},
TITLE = {{Local Confluence for Rules with Nested Application Conditions based on a New Critical Pair Notion}},
YEAR = {2010},
NUMBER = {2010-7},
INSTITUTION = {Technische Universität Berlin},
URL = {http://www.eecs.tu-berlin.de/fileadmin/f4/TechReports/2010/tr_2010-07.pdf},
PDF = {uploads/pdf/LEHOG10-TR.pdf},
OPTacc_pdf = {},
ABSTRACT = {Local con
uence is an important property in many rewriting
systems. The notion of critical pairs is central for being able to verify
local con
uence of rewriting systems in a static way. Critical pairs are
dened already in the framework of graphs and adhesive rewriting sys-
tems. These systems may hold rules with or without negative application
conditions. In this paper however, we consider rules with more general
application  conditions  |  also  called  nested  application  conditions  |
that  are  known  to  be  equivalent  to  nite  rst-order  graph  conditions.
The classical critical pair notion denotes con
icting transformations in a
minimal context satisfying the application conditions. This is no longer
true for combinations of positive and negative application conditions |
an important special case of nested ones | where we allow that critical
pairs do not satisfy the application conditions. This leads to a new notion
of critical pairs which allows to formulate and prove a Local Con
uence
Theorem for rules with nested application conditions in the framework
of  adhesive  rewriting  systems  based  on  the  DPO-approach.  It  builds
on a new Embedding Theorem and Completeness Theorem for critical
pairs based on rules with nested application conditions. We demonstrate
this new theory on the modeling of an elevator control by a typed graph
transformation system with positive and negative application conditions.}
}