Bounded Reversibility in HOpi

The higher-order causally-consistent reversible π-calculus, known as roll-π, enables the rollback of arbitrary past actions while preserving causal consistency – ensuring that effects are undone before their causes. This prevents the occurrence of actions without justifications, even after a rollback. However, in practical scenarios, not all events can be reversed; for example, once a document is printed, it cannot be unprinted. To better model real-world constraints, we introduce broll-π (boundedroll-π), an extension of roll-π that limits reversibility. Our approach imposes two key restrictions: spatial bounds, which prevent certain processes from being affected by rollbacks, and temporal bounds, which restrict how far back in time a rollback can go. Bounded reversibility allows for more realistic and controlled rollbacks in computational systems. In this paper, we provide an informal introduction to broll-π and discuss its implications for modeling reversible processes in practical applications.