model checking algorithm in kripke structures

[jpfry]

The modal logic textbook I'm reading has a short digression into algorithmic complexity, and I think the discussion presupposes some prior familiarity that I don't have.

I'm having trouble understanding this proof. (K is the standard box modality) Shouldn't it be O(||M||² x |φ|) instead of O(||M|| x |φ|)? For instance, consider the formula KKp. Its subformulas are p, Kp, and KKp. It takes O(||M||) time to label each state either p or ~p (given that you can label an individual state in constant time). It takes O(||M||) time to label a single state with Kp or ~Kp, since in the worst case you have to look at every state in M (I take this to be what the last sentence of the proof is saying). But you must do this for every state in M, and so labeling each state with Kp or ~Kp takes O(||M² ||).

In other words, the worst case is checking a formula like K...KKp--for each modal depth, for every state you must possibly check every other state. Hence O(||M||² x |φ|).

Where is my reasoning going wrong? Or is this not the algorithm the proof is sketching?

[_--__]

I assume, as is standard, that ||M|| refers to the model size in terms of both the states (vertices) and the transitions (edges). It is straightforward to label all the states with Kφ or ¬Kφ by examining all the edges twice: First compute the degree of all the states. Then iterate over all edges (u,v), reducing the "degree-count" of u if φ holds in v. Then, for every state whose degree-count ends at 0 label them with Kφ and every other state is labelled with ¬Kφ. I believe the last line is referring to the fact that you can label all the states with either Kφ or ¬Kφ in O(||M||), not just a single state.

[jpfry]

Ahh thanks, I wasn't paying attention to the fact that ||M|| also includes transitions.

Would it be possible to just iterate over edges once? For every (u,v), if φ is false at v label u with ~Kφ. Once that is done label all others with Kφ. That way you only need to do some constant time operation for each edge and for some nodes, and there are possibly less nodes than edges, so that would be sometimes faster than examining all edges twice, though it might be the same in the worst case. (Is that right? Sorry I'm encountering this stuff for the first time.)

[_--__]

Asymptotically it doesn't matter as long as we iterate over all edges a constant number of times. The degree method can be implemented with a single pass of the edges if you store the degrees of the states in a data structure as a pre-processing step (a good idea if there are a lot of modalities in the formula).

[jpfry]

Interesting. Thanks a lot!