Translating Controlled Graph Grammars to Ordinary Graph Grammars

Graph Grammar (GG) is an appropriate formal language for specifying complex systems. In a GG the system states are represented by graphs and the changes between the states are described by rules. The use of GGs is interesting as there are several techniques for the specification and verification of systems that are described in this language. Besides this, GGs have a graphical representation which is quite intuitive, making the language easy to understand even for non-theorists. Controlled graph grammars (CGGs) are GGs that allow defining a sequence of rule applications, considering an auxiliary control structure, allowing one to control the intrinsic non-determinism of this formalism. However, for this type of grammar there are no tools for verification of properties. Therefore, the aim of this paper is to translate the controlled graph grammars into ordinary graph grammars, transferring the flow control from an auxiliary structure to the state. Hence, the main contribution of this paper is to permit the use of Rodin theorem prover to carry out the verification of properties for CGG specifications. This is possible through a mechanism where a controlled graph grammar is translated into a regular graph grammar using dependencies and conflicts between rules.