Decidability Problems for Micro-Stipula
Giorgio Delzanno, Cosimo Laneve, Arnaud Sangnier, Gianluigi Zavattaro
TL;DR
μStipula provides a stateful contract calculus where clauses are activated by external calls or by time expressions. The paper proves undecidability of the unreachable-clauses problem in the full language and in its time-ahead and instantaneous fragments via reductions from Minsky machines, while identifying the μStipula^{DI} fragment as decidable by casting the system as a well-structured transition system. It also introduces a variant semantics (Tick-Plus) and leverages WSTS techniques and Dickson's lemma to obtain decidability results for this fragment. These results delineate a sharp boundary between undecidable and decidable analysis of time-aware contract behaviors, with implications for static analysis and verification of legal contracts modeled in μStipula.
Abstract
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, and the instantaneous fragment, where all time expressions evaluate to zero. On the other hand, we identify a decidable subfragment: within the instantaneous fragment, reachability becomes decidable when the initial states of functions and events are disjoint.