# An Approach to the State Explosion Problem: SOPC Case Study
## 4 Preliminaries
### Basic Definition  
**Definition 1**. : _A finite state machine: If \(M\) is a finite state machine, \(M=(S,I,O,f,g,s0)\). While \(S\) is a set of states, \(I\) is an input alphabet and \(O\) is an output alphabet. The transfer function and the output function are f, g. The initial state is \(s0\)._  
**Definition 2**. : _Kripke structure: Atomic proposition (AP) is a set of finite atomic propositions. A Kripke structure K on AP is a 4-tuple k = (\(S\), \(S_{0}\), \(R\), \(L\)), where \(S\) is a set of finite states; \(S_{0}\)\(\in\)\(s\) is the initial state set; \(R\)\(\in\)\(S\)\(\times\)\(S\) represents all state transition relationships; and \(L\): \(S\)\(\rightarrow\)\(2^{AP}\) indicates acceptable status._  
**Definition 3**. : _Linear temporal logic (LTL) [36]: The LTL is a linear temporal logic formula. Formulas of LTL are built from a set of AP (atomic proposition) using the usual Boolean operators and temporal operators X (\"next time\") and \(\cup\) (\"until\"). Given a set, AP, a formula is defined as follows:_  
_--true, false, p or \(\
eg\), for \(\mathit{p}\in\mathit{AP}\)_  
_--\(\psi\ \vee\ \varphi,\ \psi\ \wedge\ \varphi,X\psi,\ \psi\ \cup\ \varphi,\ \psi\ \stackrel{{ \sim}}{{\cup}}\ \varphi\), where \(\psi\) and \(\varphi\) are an LTL formula._  
We denote the length of a formula \(\varphi\) by \(|\varphi|\). Given a Kripke structure \(M\) and an LTL formula \(\varphi\), the model-checking aim is to determine whether all the computations of \(M\) satisfy \(\varphi\). If this is the case, we denoted it by \(M|=\varphi\), otherwise \(M|\
eq\varphi\). **Definition 4**. : _Deterministic Finite Automaton: The deterministic finite automaton will often be referred to by its acronym: deterministic finite automata (DFA). It shows that on each input there is one and only one state to which the automaton can transition from its current state. We often talk about a DFA in \"five-tuple\" notation: \(M=\)(\(Q,\ \sum\ \delta,\ \ q_{0},\ F\)), where \(M\) is the name of the DFA, \(Q\) is its set of states, \(\sum\) is its input symbols, \(\delta\) is its transition function, \(q_{0}\) is its start state, and \(F\) is its set of accepting states or final states, which is a subset of \(Q\)[37]._  
**Definition 5**. : _Nondeterministic Finite Automaton [37]: \(M=\)(\(Q,\ \sum\ \delta,\ \ q_{0},\ F\)), where \(M\) is the name of the NFA, \(Q\) is its set of states, \(\sum\) is its input symbols, \(\delta\) is its transition function, \(q_{0}\) is its start state, and \(F\) is its set of accepting states or final states, which is a subset of \(Q\). The difference between the DFA and the NFA is in the type of \"\(\delta\)\". For the NFA, \"\(\delta\)\" is a function that takes a state and input symbol as arguments (like the DFA's transition function), but returns a set of zero, one, or more states (rather than returning exactly one state, as the DFA must). For example, a Bichi automaton is a nondeterministic finite automaton._  
**Definition 6**. : _The \"language\" of the DFA [37]: The \"language\" of the DFA is the set of all strings that the DFA accepts. We can define the language of a DFA \(A=\)(\(Q,\ \sum\ \delta,\ \ q_{0},\ F\)) as \(L(A)\)._  
In temporal logic model checking, we verify the correctness of a finite state system with respect to a desired behavior by checking whether a labeled state transition graph (system model) satisfies a temporal logic formula that specifies this behavior. Temporal logic model checking includes model checking based on automata theory and model checking based on CTL. The principle of model checking based on automata theory is described in Section 5.2. Model checking based on CTL is to check whether the Kripke structure is a model of CTL for a given CTL formula. When applying model verification tools, the design is generally described in VHDL and Verilog languages, while the property language is SVA. Model checking tools convert the design into a finite state machine first, then convert it to corresponding forms based on the principles of verification.