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.

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