В чем разница между живостью и прогрессом?

Question

Я знаю, что это очень академический вопрос, но я надеялся, что кто-то здесь может помочь мне получить ответ.

Я беру класс параллелизма, в котором мы используем LTS и FLTL. В одном из наших заданий задается вопрос: "Приведите пример свойства живучести, выраженного формулой FLTL, который нельзя выразить как свойство прогресса". Просто чтобы уточнить, я не хочу ответа на этот вопрос.

Моя проблема в том, что я всегда думал о 2 как 1:) Так что, чтобы ответить на вопрос, мне нужно знать разницу между свойствами прогресса и живучести.

Любая помощь будет принята с благодарностью:)

Answer 1

Свойство живучести - это когда вы определяете, что в какой-то момент в будущем программа выполнит заданную часть программы. В FSP вы можете определить большинство свойств жизнеспособности как свойство прогресса, но в своем назначении вы должны придумать пример, где вы выражаете свойство жизнеспособности как FLTL, но вы не можете сделать это как свойство прогресса.

Вы должны найти определение формулы FLTL и свойства прогресса в FSP, чтобы увидеть, как они отличаются, а затем придумать пример, в котором вызвано некоторое ограничение в свойстве прогресса FSP, которое нельзя выразить как единое целое.

Более того, я просто немного об этом прочитал, и, похоже, что в свойстве progress FSP вы не можете описать "слабое" свойство жизни, например, когда происходит действие "enter", тогда могут произойти другие действия, но в конце концов происходит действие "выход". Это нельзя описать как свойство прогресса, потому что вы можете только описать особенности, такие как "вход" и "выход", и в предположении справедливости они оба будут происходить бесконечно часто, но в FLTL это возможно скажем, что [](enter -> <>exit), это означает, что всегда, когда происходит "вход", в конце концов случается "выход". В этом большая разница в формализме FSP и FLTL.