Using Matrix Graph Grammars for the Analysis of Behavioural Specifications: Sequential and Parallel Independence

In this paper we present a new approach for the analysis of rule-based specification of system dynamics. We model system states as simple digraphs, which can be represented with boolean matrices. Rules modelling the different state changes of the system can also be represented with boolean matrices, and therefore the rewriting is expressed using boolean operations only.The conditions for sequential independence between pair of rules are well-known in the categorical approaches to graph transformation (e.g. single and double pushout). These conditions state when two rules can be applied in any order yielding the same result. In this paper, we study the concept of sequential independence in our framework, and extend it in order to consider derivations of arbitrary finite length. Instead of studying one-step rule advances, we study independence of rule permutations in sequences of arbitrary finite length. We also analyse the conditions under which a sequence is applicable to a given host graph. We introduce rule composition and give some preliminary results regarding parallel independence. Moreover, we improve our framework making explicit the elements which, if present, disable the application of a rule or a sequence.