# An Asymptotic Cyclicity Analysis of Live Autonomous Timed Event Graphs
## 3 Transformation from a TEG to Its Precedence Graph
All places included in the set of the upstream places of \(t_{o}\) but not belonging to \(S\) is denoted as \(S^{\prime}\) (\(S^{\prime}=~{}^{\bullet}t_{o}-S=\{p_{jo}|p_{jo}\in S^{\prime}\}\)). Under this assumption, the \(r\)th firing epoch of \(t_{o}\) after applying Rule 4 is changed from Equation (6) to Equation (7):  
\[t_{o}^{r}=\max\{\max_{p_{jo}\in S}\{H(p_{io})\}+t_{i}^{r-M},\max_{p_{jo}\in S^{ \prime}}\{H(p_{jo})+(^{\bullet}p_{jo})^{r-M_{o}(p_{jo})}\}\}. \tag{6}\]  
\[t_{o}^{r}=\max\{\max_{p_{jo}\in S}\{H(p_{io})\}+t_{i}^{r-M},\max_{p_{jo}\in S^{ \prime}}\{H(p_{jo})+(^{\bullet}p_{jo})^{r-M_{o}(p_{jo})}\}\}. \tag{7}\]  
If the firing epochs of the other transitions except for \(t_{o}\) are the same as before, the firing epoch of \(t_{o}\) is also the same. Therefore, by Definition 1, the TEGs are equivalent. This paper proposes four rules to simplify the equivalent TEG. If we repeatedly apply the transformation rules proposed in this paper, we can finally derive a TEG equivalent to the original TEG to satisfy the properties of the precedence graph. We have already proved that a transformed TEG is always equivalent even after applying any of Rules 1-4. Therefore, we now show that repeatedly applying rules can make a TEG eventually satisfy the precedence graph's properties. In other words, every place has exactly one token in the final TEG, and the number of places directly connecting any two transitions is at most one. To prove that every place has exactly one token, we first show that any place has at most one token by contradiction. In other words, we hypothesize that there remains a place with two or more tokens no matter how often the rule is applied. In this case, we can decrease the number of tokens to one by applying Rule 1 to a place with multiple tokens. This decrease violates the hypothesis that, no matter how much the rule is applied, a place with multiple tokens cannot be removed. Therefore, we can always make the number of tokens fewer than one in all places. Next, we prove that there is at least one token in every place. The event graph, which this paper considers, is autonomous, so every place has its input transition. Therefore, we prove that every place has at least one token by showing that every transition has only its downstream places with tokens. When there is a transition with a downstream place without tokens, we divide the cases by the number of its downstream places. If the transition has only one downstream place without tokens, we can remove the transition using Rule 2. After that, a TEG has no transition, whose downstream place has no token. If the transition has multiple downstream places, we can remove a downstream place without tokens by applying Rule 3. If the transition has multiple downstream places with no tokens, we can remove them by applying Rule 3 repeatedly until every downstream place has at least one token. This way, we can make sure every place has at least one token. Finally, we prove by contradiction that there is at most one place that directly connects two arbitrary transitions. Expressly, we assume that no matter how many times rules are applied, there still remain multiple places that directly connect two transitions. We can make the number of tokens in those places at most one by Rule 1. If a place with more than two tokens exists, it does not link directly between the transitions because the place is replaced with a series of other places and transitions. Next, places that connect directly connected transitions are merged according  
Figure 7: Illustration of Rule 4.  
to the number of tokens by Rule 4. After applying Rule 4, if the places are merged into one, the assumption that we cannot merge places between two transitions into one is violated. If there are two places, one place has a token and the other has no token. Rule 3 can make it so there is only one place between the transitions by removing the place without tokens, so this situation also violates the assumption.