Как вы читаете набор атомарных предложений?

Question

Мне дана вышеуказанная система для атомарных высказываний {a,b,c}.

Затем я должен сказать, что некоторые формулы LTL имеют место (например, ♢☐c).

Я понимаю, что означают формулы LTL (в конечном счете, всегда с), но я понятия не имею, как прочитать диаграмму и связать ее с LTL.

Я предполагаю, что это похоже на блок-схему, в которой мы начинаем сверху слева, /{a} и может пройти через разные состояния. Но что каждый из них означает разделить на a?

Answer 1

Похоже на FSM/ преобразователь, а не на структуру Крипке. Ввод / вывод или, в более общем смысле, предусловие / постусловие - это общее обозначение для FSM и его родственников. Предпосылкой / Постусловие (a and b and ...) / (x and y and...), Так a в состоянии q1, Только в следующих штатах b в 4 квартале или b and c или q3. Может быть, конечно or вместо and при условии, что в противном случае система может остановиться.