Modal logic II: FRAMES ⟨13,06⟩—optional

Necessarily true = true in every possible world. Frames allow us to sort worlds: which worlds do we have access to in our frame? Is the actual world included in our frame? If so, any necessary truth (= true in every possible world) will be true in the actual world, too.

This video gives an introductory overview to these notions, which is preparatory to further work in modal logic.

[shawnxihaowu]

Awesome! Can't wait for the next video!

[robfielding]

This gets to the heart of what confuses me about Kripke structures. In temporal logic, stating a next value transition as variable re-assignments like: "x'=x+1" is creating a transition from the state where state "x" to state with "x+1". I do presume (in TLA fashion) that a state is a combination of its variables. If x and y can all take on values from 0..9, then there are 100 states named like [x, y]. in TLA you can have a big \/ structure of /\ statements, where "x' = x + 1" is the same as drawing an arrow.

If we have multi-modal logic, then the different modes also need to ride on top of this state machine. There are multiple sets of diamond-box operators that are duals interdefined with each other. If you are using diamond-box in the sense of possibility, and have state machines:

A -> B -> C
B -> A
C -> D
D -> E -> F
F -> D -> D
F -> F

when it is temporal, this is a PROCESS that evolves over time. even more, when you have multiple state machines, some can have "c!5" for "send the value 5 on channel c" and a different process "c?z" to "receive a value of channel c into variable z". overall, most formal methods systems are made of communicating state machines like this, with temporal logic assertions. but try to make the logic more general with different modalities; and you get state changes that didn't come from the temporal modalities.

You get from A to B by re-assigning the value of a proposition. And I suppose that if you can reach something, you can say that it is possible. and if a statement is always true, then that's a necessary condition.

One other thing that is really critical with temporal logic is that if you cannot optionally put probabilities on state changes; then you cannot do more than mere safety/liveness statements. You want to be able to do things such as measuring latency and queue sizes. For that you need probabilities on non-deterministic choices, and possibly dwell-times, to measure how long things take.