More on Nonregular PDL: Finite Models and Fibonacci-Like Programs

: We continue research on enriching propositional dynamic logic (PDL) with nonregular programs. Previous work indicates that the general problem of characterizing those extensions for which PDL becomes undecidable is probably very hard. After observing that any nonregular extension increases the expressive power of PDL, we concentrate on one-letter extensions. First, we address the issue of finite models: A general condition is formulated, and is proven to be sufficient for a one-letter extension to violate the finite model property. We show the condition to hold in several cases, including all polynomials, sums of primes, and linear recurrences. We then build on a technique of Paterson and Harel, and show that the validity problem for PDL enriched with any Fibonacci-like sequence is \Pi 1 1 -complete. 1 Introduction Propositional dynamic logic (PDL) was introduced by Fischer and Ladner [FL], based upon the first-order version of Pratt [P1]. It is a direct extension of the propositio..