Decidability Problems for Micro-Stipula
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913805877903360 |
|---|---|
| author | Delzanno, Giorgio Laneve, Cosimo Sangnier, Arnaud Zavattaro, Gianluigi |
| author_facet | Delzanno, Giorgio Laneve, Cosimo Sangnier, Arnaud Zavattaro, Gianluigi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_16703 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Decidability Problems for Micro-Stipula Delzanno, Giorgio Laneve, Cosimo Sangnier, Arnaud Zavattaro, Gianluigi Logic in Computer Science Formal Languages and Automata Theory 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. |
| title | Decidability Problems for Micro-Stipula |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2504.16703 |