# Union Models for Model Families: Efficient Reasoning over Space and Time
## 6 Analysis and Reasoning with Model Families
### Reasoning Tasks
#### 6.1.1 RT1: Property Checking  
Property checking of models aims to verify whether or not a model satisfies a particular property. Given a model \(m\) and a property \(p\), the result of property checking is either True if \(m\) satisfies \(p\) or False otherwise. For instance, a modeler may want to check whether or not a group of state machine diagrams contains self-looping edges, or she may check whether there exist two or more different actors in a GRL model family that contain the same goal. In these scenarios, property checking is beneficial to help modelers understand, for example, what is common between model versions or variations that violate a property. In this section, we limit ourselves to language-independent syntactic properties (which describe the structure of models) other than semantic properties (which describe the behavior of models, e.g., traces). The rationale behind this scoping is because our approach aims to be applicable to any metamodel-based modeling language. However, while there exists a standard approach for defining the syntax of a modeling language (i.e., through metamodeling), there is no common approach for specifying semantics. Thus, we limit our approach to checking those properties related to a language syntax independently from any language specificity. Hence, \"property\" here means \"syntactic property\". [PERSON] [10] further discusses and evaluates semantic aspects for one particular language. To perform property checking, we assume that a property \(p\) (expressed in any constraint language such as FOL or OCL) can be grounded over the vocabulary of models. Hence, a corresponding propositional formula \(\Phi p\) can be obtained. For example, given a well-formedness constraint \(\Phi p=\{\forall t:\textit{Transition},\exists s:\textit{State}\mid t.src=s\}\), it can be grounded over the vocabulary of the model in Figure 23 as follows:  
As can be noticed, the example considers the graphical representation of the state machine presented in the canonical form in Figure 6b, where transitions T1 and T2 are represented here as directed edges between states and not as nodes. Formally speaking, given the propositional encoding of both models (Section 5) and properties, the task of property checking can be defined as follows:  
**Definition 12**. : _Property Checking: Given a model \(m\), property \(p\), and their respective propositional encodings \(\Phi m\) and \(\Phi p\), we check whether the expression \(\Phi m\wedge\Phi p\) is satisfiable or not using a SAT solver._  
For RT1, inspired by [PERSON] et al. [23], we checked the \"_cyclic composition property_\", which ensures that \"the model does not contain self-looping edges\", i.e., \(\Phi p=\{\forall e:E_{G},src_{G}(e)\
eq tgt_{G}(e)\}\). It is important to highlight here that checking the self-looping edge property in individual models and in their \(M_{U}\) is a simple reasoning task that always produces the same result; that is, if a self-looping edge exists in any of the individual models, then it will be detected in the \(M_{U}\) that captures these individual models, and vice versa. This case, however, is not necessarily true for other properties, such as for example the general acyclicity property. Figure 23: An example of propositional encoding of a model (\(\Phi m\)). Figure 24 shows two simple state machine models that are acyclic (i.e., cycle-free) along with their union model \(M_{U}\) that is not acyclic (i.e., has a cycle). In this scenario, checking the acyclicity property in individual models M1 and M2 produces a different result than checking the same property in \(M_{U}\). To address this issue, there is a need to explicitly consider annotations on elements during property checking to determine the actual occurrence of cycles. For instance, if the link in model M1 is annotated with <v1> and the link in M2 is annotated with <v2>, then both links in \(M_{U}\) will be considered as different and not as an actual cycle, even though they seem to constitute a structural cycle.