These are the liveness manifestos by participants and should-be participants in the workshop.

1. Wang Yi:
   - Safety properties = those that can be checked with reachability analysis
   - Liveness: properties = those that can not be checked without loop detection

   It seems that liveness is very much related to QoS properties e.g. "Over time, every 100 events that occur, there must be at least 10 good ones". By the way, is this a QoS property? Or is it kind of "bounded QoS property"? But the property can not be checked without look detection due to the constraint "Over time".

2. Moshe Vardi:
   Liveness is used in two settings. First, as has been argued by Lamport, in certain situations it is undesriable to use the nextime connectives. In such situations we want event-based specifications rather than cycle-based specification. This forces us to use liveness properties. Second, liveness properties are used to abstract away from messy safety properties. For example, it is easier to check that
   "ALWAYS (req IMPLIES EVENTUALLY grant)" then to check
   "ALWAYS (req IMPLIES NEXY[100] grant)".

3. Jurgen Giesl:
   To me, a "liveness property" is the same as an "eventuality property", i.e., the property that eventually (after a finite number of steps) some requirement holds. Liveness (in particular, in infinite-state systems) is closely connected to termination. On the one hand, termination is a special liveness property which is essential for software verification. On the other hand, techniques for termination analysis may be useful to verify other liveness properties as well.

4. Ken McMillan:
   [Oral statement]
   Liveness is mainly useful for debugging -- ruling out certain class of errors. E.g., in the finite-state case, liveness helps to rule out that a program does what you don't want it to do, as opposed to proving a program that it what you want it to do. You never want liveness, it's just all that you can get. Nobody lives to 'eventually', however, it does cover bugs in abstraction.

5. Allen Emerson:
   I do believe in liveness, but I think it is possible to put up a pretty good argument that it is probably an unnecessary concept.

   Reasonable attitudes about liveness in software verification:

   1. It is unimportant from an academic standpoint; rather, it is a marketplace issue. That is, liveness is performance in practice.
   2. In some cases it is important, e.g. in real-time and embedded systems. We have promptness requirements - AG(request ==> AF^{<=9}grant) But those are really safety properties.

6. Neil Jones:
   The key liveness problems are to ensure that:
   1. A system can continue to provide services
   2. Usage of resources cannot grow unboundedly

   BOTH must hold for a system to be truly "live".

7. Neil Jones:
   Without safety, liveness is illusory;
   Without liveness, safety is ephemeral.

8. Armin Biere:
   No need for dedicated model checking algorithms for liveness.
   Even for infinite state systems, liveness can be transformed to safety.
   No liveness without fairness in the finite case.

9. Bernard Boigelot:
   I think that most of the properties that need to be checked in the "real world" involve explicitly bounded time, and thus can be reduced to checking safety for the system coupled with a suitable observer.

10. Andreas Podelski:
    The issue "liveness less useful than safety" becomes obsolete once we have shown that the good methods for checking safety are, in fact, methods for checking liveness (we are working on it).

11. Leslie Lamport:
    Here are the problems with liveness I know, and why they are or are not serious.

    Problem 1: Knowing that something will eventually happen isn't particularly useful; we'd like to know that it happens before the sun explodes in a few billion years.

    Not Serious: Proving real-time bounds complicates the model, and it's usually better to verify the weaker property of eventual progress and catch performance errors like long termination time in other ways. Since we're usually interested in average performance, testing is probably good enough for that.

    Problem 2: Most real systems don't satisfy liveness properties. If it's always possible that a message I send will be lost, then there's no way to guarantee that the message will eventually be received.

    Not Serious: The primary purpose of checking properties is to catch bugs and gain confidence in the system. If we believe that the only reason a message is never received is because the communication channel drops all copies of it, then we should check that belief. We can do that by showing that, if a message sent infinitely often on the channel is eventually delivered, then the message is eventually received. This check tells us something interesting about the system. It doesn't mean that every message is eventually received.

    Problem 3: When model checking their systems, engineers will always use a model that is as accurate, and hence as complicated, as possible for which they can check large enough instances of their system to find bugs. Since the inherent complexity of checking liveness is greater than that of checking safety, they can check more complicated and hence more useful models by checking only safety properties.

    Somewhat Serious: Engineers will never be able to catch subtle liveness errors of the models that interest them the most. However, when just checking safety, it's easy to make an error in your model that prevents some behaviors that should be possible. Deadlock detection and coverage checking (seeing that all actions are executed) offers only a very limited protection against such errors. The only way to catch them is by checking liveness--preventing possible behaviors will result in violation of liveness properties. Since those errors are rather gross, it's likely that they can be found by checking small instances of the models--instances that are too small (for example, use too few processes) to catch subtle bugs.

    Problem 4: More than 90% (probably more than 95%) of the errors in real systems are violations of safety properties. (Most violations of liveness in systems are due to deadlock, and absence of deadlock is a safety property.) So it's not worth the effort of checking liveness.

    Sometimes Serious: If you're doing model checking, then the extra work involved in checking liveness is being done by the computer, and computers are cheap. However, this is a real problem if you're writing very rigorous proofs. Rigorous reasoning about liveness is tedious. The pain to gain ratio of proving liveness is so high that, because most errors are caught by checking safety, it is almost always a better idea to spend scarce manpower on proving safety rather than liveness.

12. Prasad Sistla:
    Roughly speaking, Liveness properties assert that some thing good eventually happens. Such properties are different from real-time properties where one specifies a bound on the time before the occurrence of the good thing. Proving or checking liveness properties of concurrent systems is necessary due to many reasons. Consider a system of concurrent processes that are cooperating with each other. If these system of processes are running on a single computer, as multiple threads, we do not know how often these processes are scheduled to execute. That is, we do not know the scheduling policy of the operating system of the host computer. Even if the processes are running on different computers, we may not know the relative speeds of the individual computers. We may want to make the barest minimum assumptions about these issues, such as fairness, i.e. every process is executed infinitely often. Under these assumptions, we can only prove liveness properties.

    There are many other situations liveness properties become important. In communication systems with lossy channels, we make certain types of fairness assumptions about the loss of messages, i.e. if a message is tarnsmitted infinitelt many times then it will be received infinitely often. In all such systems, in general, we can only prove liveness properties.

13. Javier Esparza:
    {Liveness and partial-order semantics}
    Consider the property $Fa$, meaning that eventually the action $a$ happens. $Fa$ obviously holds for the process $P = a.0$ (I use CCS notation). However, it does not hold for $P|Q$, where $Q = b.Q$, because of the execution $b^\omega$. But $P$ and $Q$ can be systems at different locations and having nothing to do with each other. Just by \emph{conceptually} putting two systems together, the property $Fa$ ceases to hold.

    One can argue that the problem is solved by adding a weak fairness assumption: if $a$ is continuously enabled, it must eventually be taken. However, this is not always desirable. In particular, this fairness assumption will also exclude the execution $b^\omega$ in the system $P' = a.0 + b.P'$. But $P'$ is not a distributed system, just one which chooses between $a$ and $b$, and we may want to consider the possibility that the system always chooses $b$.

    One can then argue that the fairness assumption should be: Parallel composition is weakly fair, choice is not. But interleaving semantics does not distinguish between the two. In particular, bisimulation semantics identifies the system $P|Q$ above and the system $P'' = a.Q + b.P''$,

    I have always considered this simple argument (which is probably folklore, and I got from Mogens Nielsen and Wolfgang Reisig) a very good motivation for partial-order semantics. Unfortunately, I don't think that research on partial-order semantics has produced a convincing solution. Allan Cheng and Mogens Nielsen published a paper some years ago on model-checking a process algebra with a weakly fair parallel operator, but the resulting algorithm was rather complicated. Wolfgang Reisig has developed some pragmatic rules for dealing with these problems, and produced some beautiful examples, but I don't find the results satisfactory from a mathematical point of view. This seems to be one of those frustrating problems which are hid under the carpet because nobody can find a really good solution.

    {Teaching liveness in lab courses}
    One of the things I always found difficult about liveness is its unstable behaviour under refinements. In particular, the models we use for verification purposes often abstract from the mechanisms used for synchronization. We just assume that the systems decide when and with whom to synchronize by some protocol. This is usually pretty harmless when dealing with safety properties, but not for liveness properties. For instance, if we refine the synchronization model by introducing busy-waiting loops, liveness properties may cease to hold. This can be solved by adding new fairness assumptions. However, these assumptions slow the algorithms down. For instance, we know that a conjunction of fairness assumptions can make B\"uchi automata explode.

    These problems are well-known, and here I just want to mention that they make liveness hard to \emph{teach}. In lab courses on automatic verification students should model systems and then verify them. It's very difficult to find good examples with non-trivial liveness properties that are reasonably easy to model and verify. In most cases, non-trivial means too hard!

14. Muller Olm:
    1) Liveness properties are crucial for the safety of airplanes.
    2) Paradoxically, F dead is a liveness property. It even appears to be true for animals and humans...

15. Kim Larsen:
    For timed systems, reachability testing is what need and what you can afford. Reachability testing is expressive enough to cover liveness in practise (i.e. time bounded liveness) and an increase in expressive power will result in a complexity penalty (unless PSPACE=EXPTIME).

16. From Nielson and Nielson's:
    In principle termination analysis is easy: find a well-founded ordering and prove that calls decrease with respect to the ordering.

17. From a fortune cookie Pnueli got:
    Many a false step is made by standing still.

18. Orna Kupferman
    Liveness is whatever prevents an empty system from being correct.
    Examples: a need to interact with an environment, properties that are not invariants, existential (even safety) properties.

19. Byron Cook:
    Engineers without backgrounds in formal verification often want to check liveness properties. Engineers with formal verification experience have been taught only to think in terms of safety.

20. Parosh Abdulla:
    The traditional definition of liveness "something good will eventually occur" is not very useful for an engineer. It is not satisfactory to know that your program will terminate within one year. Bounded liveness is practically more relevant, but it is a safety property.

    For certain classes of systems, checking liveness cannot be reduced to checking safety. The latter is decidable while the former is not.

21. Bernhard Steffen:
    Liveness: guarantee of observable progress.

22. Lenore Zuck:
    Usually: no bad cycles
    Unfortunately: that's not always enough

23. Hardi Hungar:
    Liveness is what remains if one abstracts away the time bounds which usually come with every response property.

24. Hardi Hungar:
    1. A liveness property is useless in practice if it is not accompanied by bound
    2. A liveness property accompanied by a bound is a safety property
    3. Consequence of the above: There is no liveness property which is useful in practice
    

25. Radu Grosu:
    Safety:
        1. Reachability
        2. A property whose language can be described with an FSM
    Liveness:
        1. Cycle (lasso) detection
        2. A property whose language cannot be described with an FSM (one needs a Buchi omega-word automaton)