# CSI-5174 - Assignment 1B: Liveness and Temporal Logic

*Given: Sept. 23 - - Due: Sept. 30*

### Note: This is a continuation of Assignment 1.

**Q1 - In the system of Assignment 1, the behavior of CreateC is not live:** We consider the temporal logic formula (in **linear** temporal logic) **newC implies <> startC **, which says that once an interaction **newC** happens, eventually **startC** will happen. Please explain why this formula is not true for the system of Assignment 1.

**Q2 - Introducing fairness for jobs of type C: Please change the behavior of the components PerformA and PerformB **is such a manner that they participate in rendezvous with the interaction **newC** of the **CreateC** component. The behavior of **PerformA** and **PerformB** should be such that the **newC** interaction would be possible whenever **CreateC** would like to perform this action, and once this action is performed, the interaction **startC** should have priority over the actions **startA** and **startB** such that the action **startC** could be eventually executed after a **newC** interaction has taken place.

**Q3 - Please explain why the temporal formula of Q1 is true for your revised system of Q2.**