One of the benefits of using executable specifications such as Behavioral Programming (BP) is the ability to align the system implementation with its requirements. This is facilitated in BP by a protocol that allows independent implementation modules that specify what the system may, must, and must not do. By that, each module can enforce a single system requirement, including negative specifications such as "don't do X after Y." The existing BP protocol, however, allows only the enforcement of safety requirements and does not support the execution of liveness properties such as "do X at least three times." To model liveness requirements in BP directly and independently, we propose idioms for tagging states with "must-finish," indicating that tasks are yet to be completed. We show that this idiom allows a direct specification of known requirements patterns from the literature. We also offer semantics and two execution mechanisms, one based on a translation to B\"uchi automata and the other based on a Markov decision process (MDP). The latter approach offers the possibility of utilizing deep reinforcement learning (DRL) algorithms, which bear the potential to handle large software systems effectively. This paper presents a qualitative and quantitative assessment of the proposed approach using a proof-of-concept tool. A formal analysis of the MDP-based execution mechanism is given in an appendix.

翻译：使用可执行规约（如行为编程，BP）的益处之一在于能够使系统实现与其需求保持一致。BP通过一种协议实现这一目标，该协议允许独立实现的模块分别指定系统可以、必须以及不得执行的行为。由此，每个模块可强制执行单一系统需求，包括“在Y之后不得执行X”等负向规约。然而，现有BP协议仅支持安全需求的强制执行，不支持“至少执行三次X”等活性属性的执行。为直接在BP中独立建模活性需求，我们提出了一种标记状态“必须完成”（must-finish）的习惯用法，以指示尚未完成的任务。研究表明，该习惯用法能够直接规约文献中已知的需求模式。我们还提供了相应的语义及两种执行机制：一种基于向Büchi自动机的转化，另一种基于马尔可夫决策过程（MDP）。后者可利用深度强化学习（DRL）算法，有望有效处理大规模软件系统。本文通过概念验证工具对所提方法进行了定性与定量评估，并在附录中给出了基于MDP执行机制的形式化分析。