The problem of the dining philosophers is a classical example to

illustrate synchronization problems resulting from the execution of concurrent

systems. Consider the following protocol:

A group of philosophers sits $($counter$-$clockwise$)$ at a round table with

something to eat in the middle.

Between each pair of philosophers lies a fork.

A philosopher either thinks, waits $(=$ wants to eat$),$ or eats.

In order to eat, a philosopher needs exactly two forks.

A philosopher can only pick up the forks to his left and right.

A philosopher can only pick up one fork at a time $($not both at once$).$

A philosopher only puts a fork back on the table after he has finished

eating.

When a philosopher gets hold of his second fork, he starts to eat for a

fixed amount of time.

After he has finished eating, he puts both forks together back on the

table and starts thinking again.

With each step of the protocol, exactly one philosopher change its state.

For example, no two philosophers pick up $($different$)$ forks at the same

time.

a$)$ Assume three philosophers. Provide the $($discrete$-$time$)$ model as LTS$.$

b$)$ An important property of protocols is freedom of deadlocks. A deadlock in

a discrete$-$time system is a system state where the system gets stuck and

no progress is possible. Is the protocol deadlock$-$free? Can you show the

property for any number $n?$

c$)$ A fork can not be held by multiple philosophers at once. Provide the safety

property in LTL for your model.