The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908343664115712 |
|---|---|
| author | Chodil, Miroslav Kučera, Antonín |
| author_facet | Chodil, Miroslav Kučera, Antonín |
| contents | The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts, the decidability of PCTL satisfiability and validity problems remained unresolved for 30 years. We show that both problems are highly undecidable, i.e., beyond the arithmetical hierarchy. Consequently, there is no sound and complete deductive system for PCTL. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_19207 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable Chodil, Miroslav Kučera, Antonín Logic in Computer Science The Probabilistic Computational Tree Logic (PCTL) is the main specification formalism for discrete probabilistic systems modeled by Markov chains. Despite serious research attempts, the decidability of PCTL satisfiability and validity problems remained unresolved for 30 years. We show that both problems are highly undecidable, i.e., beyond the arithmetical hierarchy. Consequently, there is no sound and complete deductive system for PCTL. |
| title | The Satisfiability and Validity Problems for Probabilistic Computational Tree Logic are Highly Undecidable |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.19207 |