← 研踪 PaperTrailarXiv:2611.02971 · v1
Propositional Dynamic Logic with Program Costs
首次提交 2026-11-02 19:39
版本更新 2026-11-02 19:39
雷达观测 2026-11-04 23:42
摘要
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}$.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-02 19:39 · 最新观测版本
Propositional Dynamic Logic with Program Costs
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}$.
查看此版本解读 →查看此版本原文 ↗