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.

翻译：我们提出了一种支持交替、不完全信息和递归的新型编程模型。我们通过新颖的编程构造——紧迫性标注来建模不完全信息，这些标注装饰了（天使性和恶魔性）选择算子，并控制选择的执行顺序。我们的贡献在于研究了紧迫性程序上下文等价性的标准概念。第一个主要结果是基于完备且可靠的公理化系统，对这些关系给出了完全抽象的特征刻画。该公理系统清晰揭示了不完全信息如何分布于完全信息之上。第二个主要结果是确定了这些关系的可计算性状态。值得注意的是，我们证明了对于最大紧迫性为h的程序，当正则可观测性作为输入给出时，上下文预序是(2h-1)-EXPTIME完全的；而当正则可观测性固定时，该预序是PTIME完全的。我们的发现为超模型检测——这一安全领域的突出问题——带来了新的可判定性结果。