Complexity of checking the existence of counter-example at bound k using bounded model checking with SAT

This is a memo of complexity analysis of "checking the existence of counter-example at bound k using bounded model checking with SAT". (And this is different from the complexity of bounded model checking using SAT).

In BMC using SAT, model checking problem is reduced to SAT problem. That is, model checking problem is translated to a propositional formula, and then its satisfiability is solved by SAT solver. In SAT problem the complexity depends on the number of boolean variables in a given formula. Accordingly it suffices to analyze the number of boolean variables in formula obtained by reducing the model checking problem into propositional formula.

In ??, two kinds of translations are proposed, syntactic and semantics translation, and each of them has different complexity.

The complexity of syntactic translation is as follows.
Let S be the number of states of Kripke model, k be the bound of length, and |\phi| is the length of LTL formula, then The number of the boolean formula is as follows:

O(k * |log(S)| + (k+1)^2) * |\phi|)

The complexity of semantics translation is as follows.
The semantic translation results in a propositional formula with O(k · (|v|+|p|)) variables, where v and p are the sets of variables of M and ϕ,
respectively.