please show all work thank you Express the following specifi

please show all work. thank you.

Express the following specification as LTL formula on the alphabet {p, d}, where p means that the button is pushed and d means that the process is currently deadlocked, and build the equivalent automaton: \"Always, if the button is pushed, a certain process will eventually be permanently deadlocked\"

Solution

p -- Button is pushed

d -- process is currently deadlocked

Hence the given statement is equivalent to

if p happens, q is definitely going to happen

So notation is

p --> q