Propositional Dynamic Logic with Program Costs
Abstract
We introduce ℕPDL, a resource-aware variant of Propositional Dynamic Logic (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 ℕPDL as our main results. We furthermore provide upper and lower complexity bounds for this logic using translations between standard PDL and ℕPDL.
Related
- Affine modal propositional logic
- Failure of Higher-Order Truth within Intuitionistic Propositional Logic
- Quantified propositional calculi and narrow implicit proofs
- A Dynamic Inventory Rationing Model for Last-Mile Delivery of Medication in Liberia's Community Health Program
- Possibilistic Logic over a Logic of Formal Inconsistency
BibTeX
@misc{manoorkar2026propositional,
title = {{Propositional Dynamic Logic with Program Costs}},
author = {Krishna Manoorkar and Wolfgang Poiger},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.02971},
eprint = {2611.02971},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.02971},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Propositional Dynamic Logic with Program Costs
AU - Krishna Manoorkar
AU - Wolfgang Poiger
PY - 2026
DA - 2026/11/02
PB - arXiv
DO - 10.48550/arxiv.2611.02971
UR - https://arxiv.org/abs/2611.02971
AB - We introduce ℕPDL, a resource-aware variant of Propositional Dynamic Logic (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 ℕPDL as our main results. We furthermore provide upper and lower complexity bounds for this logic using translations between standard PDL and ℕPDL.
ER -