On Deadlock and Fairness Decision Problems for Computations on Client-server Systems

Phenomena that inherently happen in distributed computing - some types of deadlock and fairness or starvation - are examined in a client-server model. Messages travelling between clients and a server are: request for an action, permission to start it, and termination of its execution. Deadlock-prone and (un)fair behaviours are formulated for the model and equivalence of the respective formulae to formulae expressing emptiness and finiteness of some sets generated by the model is established. From these results, some answers to decision problems for the aforesaid properties are obtained. Furthermore, equivalence between the so-called strong fairness (specified by first-order formula) and weak-fairness (second-order formula) is demonstrated