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 non-determinism, 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.
Laneve, C. (2024). Reachability Analysis in Micro-Stipula. 1601 Broadway, 10th Floor, NEW YORK, NY, UNITED STATES : ASSOC COMPUTING MACHINERY [10.1145/3678232.3678247].
Reachability Analysis in Micro-Stipula
Laneve C.
2024
Abstract
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 non-determinism, 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.File in questo prodotto:
Eventuali allegati, non sono esposti
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
