Clause-reachability is undecidable in legal contracts

Micro-Stipula is a stateful calculus in which clauses can be activated either through interactions with the external environment or by the evaluation of time expressions. Despite the apparent simplicity of its syntax and operational model, the combination of state evolution, time reasoning, and nondeterminism gives rise to significant analytical challenges. In particular, we show that determining whether a clause is never executed is undecidable. We formally prove that this undecidability result holds even for syntactically restricted fragments: namely, the time-ahead fragment, where all time expressions are strictly positive, the instantaneous fragment, where all time expressions evaluate to zero, and the determinate fragment, where the initial states of functions and events are disjoint. On the other hand, we identify a decidable subfragment: at the intersection of the instantaneous and determinate fragments reachability becomes decidable.