More on nonregular PDL: expressive power, finite models, Fibonacci 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. Consequently, we aim lower, addressing the related issues of expressive power and the finite model property. We also settle the decidability question for a nontrivial special case. Specifically, (i) the expressive power of any nonregular extension of PDL is shown to be stronger than that of regular PDL; (ii) a general condition is formulated that is sufficient for a one-letter nonregular extension to violate the finite model property, and is shown to hold in several cases, such as polynomials, sums of primes, factorial numbers, and linear recurrences; (iii) building on a technique of Paterson and Harel (1984), the validity problem for PDL enriched with the Fibonacci-like sequence 1, 4, 5, 9, 14, ..., is shown to be Π₁¹-complete