Contextual Equivalence for Alternation and Urgency
share
We propose a new programming model with support for alternation, imperfect information, and recursion. We model imperfect information with the novel programming construct of urgency annotations that decorate the (angelic and demonic) choice operators and control the order in which the choices have to be made. Our contribution is a study of the standard notions of contextual equivalence for urgency programs. Our first main result are fully abstract characterizations of these relations based on sound and complete axiomatizations. The axiomatization clearly shows how imperfect information distributes over perfect information. Our second main result is to settle their computability status. Notably, we show that the contextual preorder is (2h-1)-EXPTIME-complete for programs of maximal urgency h when the regular observable is given as an input resp. PTIME-complete when the regular observable is fixed. Our findings imply new decidability results for hyper model checking, a prominent problem in security.
READ FULL TEXT