Q3. Printer Suppose we have two users, Peter and Jane, and a single printer device Printer. Both users perform several tasks, and every now and then they want to print their results on the Printer. Since there is only one printer, only one user can print a job at a time. Suppose we have the following atomic propositions for Peter at our disposal: Peter.request ::= indicates that Peter request usage of the printer. Peter.use ::= indicates that Peter uses the printer. Peter release ::= indicates that Peter releases the printer. For Jane, similar predicates are defined. Specify in LTL the following properties: (a) Mutual Exclusion, i.e., only one user at a time can use the printer (b) Finite time of usage, i.e., a user can print only for a finite amount of time. (C) Absence of individual starvation, i.e., if a user wants to print something, he/she eventually is able to do so. (d) Absence of blocking, i.e., a user can always request to use the printer. (e) Alternating access, i.e., users must strictly alternate in printing. Explain your answers