活跃度和进度属性有什么区别？
我知道这是一个非常学术的问题，但我希望这里有人可以帮助我得到答案。
我正在上一门并发课程，其中我们使用 LTS 和 FLTL。在我们的一项作业中，给出了一个问题：“给出一个活性属性的例子，用 FLTL 公式表示，但不能用进度属性表示。”。 澄清一下，我不想要这个问题的答案。
我的问题是我总是将 2 视为 1 :) 因此，为了回答这个问题，我需要知道进度属性和活跃属性之间的区别。
任何帮助将不胜感激:)
I know this is a very academic question, but I was hoping someone here could help me get an answer.
I'm taking a concurrency class in which we use LTS'es and FLTL's. In one of our assignments a question is given: "Give an example of a liveness property, expressed as an FLTL formula, that cannot be expressed as a progress property.". Just to clarify, I don't want the answer to this question.
My problem is that I always thought of the 2 as 1 :) So in order to answer the question, I need to know the difference between progress and liveness properties.
Any help would be greatly appreciated :)
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
活性属性是指当您定义该属性时，程序将在将来的某个时刻执行程序的给定部分。在 FSP 中，您可以将大多数活性属性定义为进度属性，但在作业中，您必须提供一个示例，其中将活性属性表示为 FLTL，但不能将其作为进度属性。
您必须查找 FLTL 公式和 FSP 中的进度属性的定义，看看它们有何不同，然后提出一个示例，其中导致 FSP 进度属性中的某些限制无法表示为一个。
此外，我刚刚读了一些相关内容，看来，在 FSP 的进度属性中，您无法描述“松散”的活性属性，例如，当“输入”动作发生时，可能会发生其他一些动作，但是最终发生“退出”动作。这不能被描述为进度属性，因为你只能描述细节，例如“进入”发生和“退出”发生，并且在公平的假设下它们都会无限频繁地发生，但在 FLTL 中可以也就是说，[](enter -> <> exit)，这意味着当“进入”发生时，最终总会发生“退出”。这就是FSP和FLTL形式主义进展的巨大差异。
An liveness property, is when you defining that, at some point in the future the program will execute a given part of the program. In FSP that you can define most liveness properties as a progress property, but in your assignment you have to come up with an example where you expresses a liveness property as an FLTL, but you cannot do it as a progress property.
You have to lookup the definition the FLTL formula and the progress property in FSP to see how they are different, and then come up with an example where caused some limitation in the FSP progress property cannot express as one.
Further more, I just read a bit about it, and it seems, en the progress property of FSP, you cannot describe a "loose" liveness propety such as, when the action "enter" happens then some other could actions could happen, but eventually an "exit" action occurs. This cannot be described as a progress property, because you only can describe specifics, such as an "enter" happens and an "exit" happens, and under the assumption of fairness they will both occur infinitely often, but in FLTL it is possible to say that, [](enter -> <>exit), this means always when an "enter" occurs eventually there will happen an "exit". this is the big difference of progress in FSP and FLTL formalism.