Describe how protocols arising in systems can be described as finite state machines.
Describe a representation of finite state machines as (database) relations suitable for analysis using datalog -- that is, give a suitable schema. Try to state in as great generality as you can which properties of protocols can be expressed in datalog.
Which safety and lifeness properties, if any?
You may use (stratified) datalog with negation.
(If you are not familiar with datalog with negation, answer the following question: for which safety or lifeness properties can their negation
be expressed in datalog?)