New logic measures program costs to check computational limits
Propositional Dynamic Logic with Program Costs
Logic in Computer Science
Summary
Programs often have costs like time or memory, but traditional logics don't measure these. The authors developed a new kind of logic, called NPDL, that tracks such costs using natural numbers. This logic can say whether certain properties of a program can be reached within a specific cost limit. They also proved this logic's reasoning methods work well and can be decided by a computer. This helps understand and verify programs with resource constraints.
What this means in practice
- •For software verification teams: Determine if programs meet resource limits by reasoning about cost-bound program behaviors using a new logical framework.
- •For formal methods engineers: Analyze and verify resource-aware system properties within defined cost constraints using decidable weighted program logics.
A theory result. No direct application yet.
Authors
Krishna Manoorkar, Wolfgang Poiger
Abstract
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}$.