Adding liveness to behavioral programming: theory, implementation, and user study

Abstract This paper investigates how Behavioral Programming (BP), and executable specifications in general, can more effectively align models with requirements, addressing a key motivation behind BP’s development. While BP has traditionally supported safety requirements—defining what a system may, must, and must not do—it lacks direct mechanisms for expressing liveness requirements, which ensure that certain tasks are eventually completed. We introduce a “must-finish” idiom for BP, allowing explicit specification of liveness requirements. We demonstrate how this approach allows for the direct representation of common requirements patterns, supported by a user study that highlights positive outcomes, particularly in improving the alignment between software components and their corresponding requirements. While formal modeling languages that allow specification of liveness requirements are mostly used in the context of model-checking and synthesis, the focus of BP is on the executability of the model. To this end, we propose two execution mechanisms: one based on translation to Büchi automata and another using Markov decision processes (MDP), with the latter offering scalability through deep reinforcement learning. A formal analysis of the MDP-based mechanism is provided, together with qualitative and quantitative evaluations of a proof-of-concept tool.