CTL * и мю-исчисление

хорошо известно, что модальный $\mu$ -calculus является одной из наиболее выразительных временных логик для выражения свойств деревьев / графов, и что CTL * строго менее выразителен, чем $\mu$ -исчисление.

Здесь я хотел бы попросить пример $\mu$ формула вычисления, настолько простая, насколько это возможно, которая не выражается в CTL *, и, надеюсь, для объяснения ее значения (формулы с фиксированной запятой быстро становятся нечитаемыми). Любая хорошая ссылка на «конкретный» простой пример также была бы отличной!

заранее спасибо

lo.logic model-checking temporal-logic mu-calculus LORE81
источник

Ответы:

Возьмите свойство пути, которое не выразимо первого порядка, например

ν x . p \land ◊ ◊ x

$\nu x.p\wedge\Diamond\Diamond x$ который говорит, что существует путь, где атомное суждение

p

$p$ удерживается на каждой четной позиции, и любая оценка может использоваться на нечетных позициях.

Сильвен
источник

Большое спасибо за этот простой ответ. Не могли бы вы также предложить ссылку в поддержку этого примера?

Еще

Хороший вопрос и ответ (+2). Взгляните на cstheory.stackexchange.com/q/16186/6424 . Я также привел пример ровности. Может быть, какой-то ответ будет относиться и к ровности.

DaveBall aka user750378

@ LORE81: ``

p

$p$ пример с четными позициями - это классика, которую вы можете найти, например, в статье Вулпера, на которую @DaveBall указал в своем вопросе. Нетрудно доказать непосредственно по индукции по формулам LTL; альтернативно, вы можете построить переходный моноид и увидеть, что он не апериодический; наконец, вы можете попробовать аргумент Ehrenfeucht-Fraïssé, хотя это подробно изложить в деталях.

Сильвен