<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Analysis Techniques for Graph Transformation Systems</article-title>
      </title-group>
      <contrib-group>
        <aff id="aff0">
          <label>0</label>
          <institution>Philipps-Universitat Marburg</institution>
          ,
          <country country="DE">Germany</country>
        </aff>
      </contrib-group>
      <abstract>
        <p>In software and system development, veri cation and validation means investigating artifacts in order to check if they ful ll the intended purposes. Graph transformation systems can be considered as precise models of computation where states are represented by graphs and state changes by rule-based graph transformations. This talk gives an overview of selected analysis techniques being available. For typed graph transformation systems, all graphs being transformation results automatically conform to the given type graph. Hence, they are type correct. Simple constraints such as multiplicities, are often taken into account as well. If a graph transformation system computes an operation, functional behavior may be intended. This means that, for each input graph, exactly one output graph is computed. Functional behavior is ensured if the following two properties hold: con uence (also called determinism) and termination. Con uence means that, given an initial graph, all transformations starting at this graph yield the same result graph. The check for con uence can be based on critical pairs specifying potential con icts and dependencies. A graph transformation system terminates if nite transformation sequences are possible only. We discuss several termination criteria for graph transformation systems. To check interesting properties of graph transformation systems, two techniques are considered: Invariants, i.e., graph-speci c properties, may be formulated in rst-order logic. A graph transformation system fullls an invariant if its start graph(s) ful ll them and all rules preserve them. If a rule causes inconsistent result graphs, it is augmented by additional pre-conditions deduced from violated invariants. While invariants are formulated for graphs, temporal properties, e.g., safety or reachability properties, are checked for graph transformation systems. By model checking techniques, all possible transformations are systematically considered and counter examples are reported.</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list />
  </back>
</article>