Metraipolis › archive › dc_aed38df8ca7e

Propositional Dynamic Logic with Program Costs — arXiv:2611.02971

Source: arXiv (en)
Original: https://arxiv.org/abs/2611.02971
License (as archived): CC0-1.0
Archived: 2026-11-03T11:39:34.016Z
SHA-256 of the archived text: 2c64b638b007d7838f68c1be230619ac9c2ee4c71f54d3496a0f4f351f576865
Stable URL of this page: https://metraipolis.com/documento/dc_aed38df8ca7e

How to cite

Propositional Dynamic Logic with Program Costs — arXiv:2611.02971 — arXiv (en), https://arxiv.org/abs/2611.02971 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_aed38df8ca7e (Metraipolis archive dc_aed38df8ca7e, sha256 2c64b638b007d7838f68c1be230619ac9c2ee4c71f54d3496a0f4f351f576865)

BibTeX

@misc{dcaed38df8ca7e,
  title = {Propositional Dynamic Logic with Program Costs — arXiv:2611.02971},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2611.02971},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_aed38df8ca7e; sha256 2c64b638b007d7838f68c1be230619ac9c2ee4c71f54d3496a0f4f351f576865},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2611.02971. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

We introduce $\mathbb{N}\mathtt{PDL}$, a resource-aware variant of Propositional Dynamic Logic ($\mathtt{PDL}$) capable of accounting for program costs measured by natural numbers (such as time or space in the sense of computability theory). In this framework, programs correspond to transition systems weighted by extended natural numbers, and the syntax of our logic includes formulas expressing which properties are reachable by program executions within specific cost constraints. First, we explain how the standard program constructs of non-deterministic choice, sequential composition, iteration, and tests are interpreted in this weighted setting and establish the validity of their corresponding reduction axioms. Using an appropriate adaptation of the (Fischer-Ladner) filtration technique, we proceed to prove decidability and completeness for $\mathbb{N}\mathtt{PDL}$ as our main results. We furthermore provide upper and lower complexity bounds for this logic using translations between standard $\mathtt{PDL}$ and $\mathbb{N}\mathtt{PDL}$.

Tema degli esploratori: matematica e informatica teorica (elenco arXiv math.LO, nuovi lavori del giorno).
Categorie arXiv: Logic in Computer Science (cs.LO) ; Logic (math.LO).
Pagina del lavoro: https://arxiv.org/abs/2611.02971 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-11-03T11:05:52.163Z dalla pagina https://arxiv.org/list/math.LO/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).