How to prove Liveness in processes.

[knowLittle]

Homework Statement

I have a question about theory of multi-processes competing for resources.
Basically, I want to know a semi-formal way to prove liveness, which informally it means that "something good must eventually happen".
For example, some process may eventually enter a critical section.

Homework Equations

I want to know how to prove this.
Can I show that there are no deadlocks or livelocks? Or show that there are livelocks and deadlocks present and in this way prove that liveness is not present in an algorithm?

The Attempt at a Solution

Thank you.

 

[Valkarie]

In order to prove liveness formally, you can use a technique known as “state-space exploration”. This involves constructing a directed graph (known as a “state-space graph”) that contains all possible states of the system. This graph is then explored using a depth-first search or breadth-first search to identify any cycles which may exist. If a cycle is found, then this indicates that a deadlock or livelock has been identified, and thus liveness has not been proven. If no cycles are found, then liveness has been proven.