We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (angelic and demonic) choice operators and control the order in which alternation is resolved. We study 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. Our second main result settles their computability via a normal form construction. 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. We designed urgency programs as a framework in which it is convenient to formulate and study verification and synthesis problems. We demonstrate this on a number of examples including the verification of concurrent and recursive programs and hyper model checking.

翻译：我们提出紧急程序（urgency programs），一种支持交替、不完全信息和递归的新编程模型。其创新在于对（天使性与恶魔性）选择算子进行装饰的紧急标注（urgency annotations），用以控制交替的解析顺序。我们研究了紧急程序上下文等价关系的标准概念。第一个主要结果是基于完全公理化系统对这些关系的完全抽象刻画。第二个主要结果通过范式构造解决了它们的可计算性问题。值得注意的是，当正则观察量作为输入给出时，对于最大紧急度为h的程序，上下文预序是(2h-1)-EXPTIME完全的；当正则观察量固定时，则是PTIME完全的。我们设计紧急程序作为便于表述和研究验证与综合问题的框架，并通过多个实例（包括并发递归程序验证与超模型检验）证明了其实用性。