Affiliations: Technische Universität Berlin, Germany, ehrig@cs.tu-berlin.de | Konrad-Zuse-Zentrum für Informationstechnik, Berlin, Germany, golas@zib.de | Carl v. Ossietzky Universität Oldenburg, Germany, habel@informatik.uni-oldenburg.de | Hasso Plattner Institut, Universität Potsdam, Germany, Leen.Lambers@hpi.uni-potsdam.de | Universitat Politècnica de Catalunya, Spain, orejas@lsi.upc.edu
Note: [] The work of this author was partially funded by the Deutsche Forschungsgemeinschaft in the course of the project - Correct Model Transformations - see http://www.hpi.uni-potsdam.de/giese/projekte/kormoran.html?L=1. Address for correspondence: Fachgebiet Systemanalyse und Modellierung, Hasso-Plattner-Institut für Softwaresystemtechnik GmbH, Prof.-Dr.-Helmert-Str. 2-3, 14482 Potsdam
Note: [] The work of this author was partially supported by the MEC project FORMALISM(ref. TIN2007-66523) and by the AGAUR grant to the research group ALBCOM (ref. 00516).
Abstract: Graph transformation systems have been studied extensively and applied to several areas of computer science like formal language theory, the modeling of databases, concurrent or distributed systems, and visual, logical, and functional programming. In most kinds of applications it is necessary to have the possibility of restricting the applicability of rules. This is usually done by means of application conditions. In this paper, we continue the work of extending the fundamental theory of graph transformation to the case where rules may use arbitrary (nested) application conditions. More precisely, we generalize the Embedding theorem, and we study how local confluence can be checked in this context. In particular, we define a new notion of critical pair which allows us to formulate and prove a Local Confluence Theorem for the general case of rules with nested application conditions. All our results are presented, not for a specific class of graphs, but for any arbitrary ℳ-adhesive category, which means that our results apply to most kinds of graphical structures. We demonstrate our theory on the modeling of an elevator control by a typed graph transformation system with positive and negative application conditions.
