Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements
Tom Yaacov, Achiya Elyasaf, Gera Weiss
TL;DR
This paper addresses the gap in Behavioral Programming (BP) for expressing and enforcing liveness properties. It introduces a must-finish idiom that marks states as requiring eventual completion, augments BP semantics with a labeling function, and defines live runs, enabling direct modeling of liveness. Two execution mechanisms are developed: a Generalized Büchi Automaton (GBA) approach and a Markov Decision Process (MDP) approach, with the latter supporting deep reinforcement learning (DRL) to scale to large state spaces. The authors map Dwyer specification patterns to BP using must-finish, demonstrate the methods on level-crossing and Sokoban benchmarks, and show DRL-based scaling is viable, while providing a formal appendix for MDP-based correctness. Collectively, the work advances BP toward correct-by-construction liveness enforcement and broadens its applicability to complex, scalable systems.
Abstract
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üchi 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.