What is the size of an LTL formula?

Question

What is generally meant by the size of an LTL formula, |p|, in terms of complexity? Number of atomic propositions, depth or something else?

Thanks in advance!!

Answer 1

In terms of complexity it makes sense to count the number of X and U operators used in the formula. Please note that you can regard operators like F, G, R and W as syntactic sugar that uses U (see Syntax of LTL).

Justification: When model checking the system you have to consider each possible future for each state of the system. So you have to consider that a sub-formula of the form X... or ...U... might be true or false. Thus, you have 2^n possibilities for each state, where n is the number of X and U operators.

More precisely, when you use e.g. Lichtenstein and Pnueli's algorithm to verify the formula, you search for strongly connected components (SCC) in a graph of a size <= s*2^n with s being the number of states.

If your LTL syntax allows past operators, too, then you can add the operators Y and S analogously.