A Boolean encoding of the Most Permissive semantics for Boolean networks

Boolean networks are widely used to model biological regulatory networks and study their dynamics. Classical semantics, such as the asynchronous semantics, do not always accurately capture transient or asymptotic behaviors observed in quantitative models. To address this limitation, the Most Permissive semantics was introduced by Paulev\'e et al., extending Boolean dynamics with intermediate activity levels that allow components to transiently activate or inhibit their targets during transitions. In this work, we provide a Boolean encoding of the Most Permissive semantics: each component of the original network is represented by a triplet of Boolean variables, and we derive the extended logical function governing the resulting network. We prove that the asynchronous dynamics of the encoded network exactly reproduces the attainability properties of the original network under Most Permissive semantics. This encoding is implemented as a modifier within the bioLQM framework, making it directly compatible with existing tools such as GINsim. To address scalability limitations, we further extend the tool to support partial unfolding, restricted to a user-defined subset of components.