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 :)
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.