Reachability Analysis in Micro-Stipula
Cosimo Laneve · 2024
Micro-Stipula is a stateful calculus defining clauses that may be either invoked by the external environment or triggered by time expressions. Because of the interplay between states, time and nondeterminism, establishing whether a clause will be ever executed – the reachability problem – is difficult. In this paper we define an analyzer that spots unreachable clauses and demonstrate its soundness.