## 2 Materials and Methods
### Background and Related Work
#### 2.1.1 Temporal Logic
For the existential operator, the property is valid for some branches being a possible result; from this branch, it is possible/probable to reach this symbol. As for universal, this property must be valid for all branches--it must always be satisfied. Also, operators like \(X\) (next), \(U\) (until), \(F\varphi\) (eventually), and \(G\varphi\) (henceforth) are also present in the grammar of this logic. Several related works can be cited, such as the study by [PERSON] et al. (2018), which models the security requirements using the CTL for the zero knowledge authentication protocol of Fiat-Shamir and verifies them through NuSMV. Regarding the following work, [PERSON] et al. (2018) validates a security architecture to prevent unauthorized access and data leakage in a multi-tenant cloud field-programmable gate array (FPGA) using CTL to verify the architecture and its configuration, in order to guarantee security in virtual machines (VMs). The authors [PERSON] et al. (2018) make formal verification of the Z-wave protocol through the ASMETA framework, using CTL together with AsmetaSMV to verify security properties in the mentioned protocol. Continuing this topic, [PERSON] et al. (2018) developed an algorithm called bulk-synchronous parallel (BSP) for on-the-fly computing, evaluating whether a structured security protocol model satisfies a CTL formula. This work addresses the issue of the cost of evaluating CTL formulas (in terms of time and space) using a parallelization approach. Finally, [PERSON] et al. (2018) present a work that models Trusted Architectures for IoT using Petri Nets and describes behaviors (prohibited and desired) using CTL to evaluate key security points within this type of architecture. Most noteworthy are [PERSON] et al., who focus on zero knowledge authentication. Nevertheless, other works of the group present important contributions to the security and evaluation of resource consumption in CTL validations. The next temporal logic is **timed computational tree logic (TCTL)**, which was proposed by [PERSON] et al. (2018) in 1993 and expresses time requirements using variables that change the time interval. Time is in the realm of reals with a differentiated form of quantification (S  
engineering process. This work used Uppaal modeling and mission description through TCTL. Finally, there is the contribution of [PERSON] [52], who works in the context of process flow based on microservices. In his work, the author brings a framework for the continuous verification of microservices based on conductor (the engine open source of microservices orchestration--[[https://netflix.github.io/conductor/](https://netflix.github.io/conductor/)]([https://netflix.github.io/conductor/](https://netflix.github.io/conductor/)), accessed on 1 July 2023), using Petri nets for modeling and TCTL for verification. Among these six studies, [PERSON] et al. [50] address the verification of smart contracts using temporal logic and security. In regards to **metric temporal logic (MTL)**, it is another approach that differs from the previous ones as it expresses temporal relations as causal [53]. The MTL was proposed by [PERSON] [54] in 1990 and complemented by [PERSON] and [PERSON] [55] in order to meet the need to express real-time properties in the model, being particularly important for this type of system [56]. Furthermore, this logic can represent both quantitative and qualitative temporal relationships [57] as well as future connectors and connectors representing past properties. Another significant feature is its two possible semantics: pointwise and continuous -, much like TCTL. While pointwise semantics represent discrete time, continuous represents time in the rational domain. Its operators are similar to those contained in the LTL. However, they adopt modifications to represent the time interval and the past.