lts - liveness 和 progress 属性有什么区别？

Question

我知道这是一个非常学术的问题，但我希望这里有人可以帮助我得到答案。

我正在学习一个使用 LTS 和 FLTL 的并发类。在我们的一项作业中，给出了一个问题：“举一个活性属性的例子，用 FLTL 公式表示，它不能表示为进度属性。”。澄清一下，我不想回答这个问题。

我的问题是我一直认为 2 为 1 :) 所以为了回答这个问题，我需要知道进度和活性属性之间的区别。

任何帮助将不胜感激 ：）

Answer 1

活性属性是当您定义它时，程序将在将来的某个时间执行程序的给定部分。在 FSP 中，您可以将大多数活性属性定义为进度属性，但在您的作业中，您必须提出一个示例，将活性属性表示为 FLTL，但您不能将其作为进度属性。

您必须在 FSP 中查找 FLTL 公式和进度属性的定义，以了解它们有何不同，然后提出一个示例，导致 FSP 进度属性中的某些限制无法表达为一个。

此外，我刚刚阅读了一些关于它的内容，似乎在 FSP 的进度属性中，您无法描述“松散”的活性属性，​​例如，当“进入”动作发生时，可能会发生其他一些可能的动作，但是最终会发生“退出”动作。这不能被描述为进度属性，因为您只能描述细节，例如“进入”发生和“退出”发生，并且在公平的假设下它们都将无限频繁地发生，但在 FLTL 中可以也就是说，[](enter -> <>exit)，这意味着当“进入”最终发生时，总会发生“退出”。这是 FSP 和 FLTL 形式主义进步的巨大差异。