This is a question on MODEL CHECKING
Express the following correctness properties in LTL. Feel free to defne propositions/variables to model the events mentioned in the question.
(a) If a parent process calls the blocking waitpid() system call then it is blocked until the child process terminates.
(b) If a process P calls down() on a binary semaphore and later process Q calls down() on the same semaphore before P calls up() on it, Q gets blocked until P calls up(), if P ever calls up().
(c) In the Singleton design pattern, an instance of the Singleton class is cre-ated at most once irregardless of how many times getInstance() method is called.