# Complexity and expressivity of propositional dynamic logics with finitely many variables

## TL;DR

This paper explores the complexity and expressive power of finite-variable fragments of propositional dynamic logics, showing that variable-free fragments are as expressive as full logics and that complexity remains unchanged.

## Contribution

It demonstrates that variable-free fragments of various PDL variants are as expressive as the full logics and that their satisfiability complexity remains the same.

## Key findings

- Variable-free fragments are as expressive as full logics.
- Complexity of satisfiability remains unchanged in variable-free fragments.
- Undecidability persists in certain PDL variants without variables.

## Abstract

We investigate the complexity of satisfiability for finite-variable fragments of propositional dynamic logics. We consider three formalisms belonging to three representative complexity classes, broadly understood,---regular PDL, which is EXPTIME-complete, PDL with intersection, which is 2EXPTIME-complete, and PDL with parallel composition, which is undecidable. We show that, for each of these logics, the complexity of satisfiability remains unchanged even if we only allow as inputs formulas built solely out of propositional constants, i.e. without propositional variables. Moreover, we show that this is a consequence of the richness of the expressive power of variable-free fragments: for all the logics we consider, such fragments are as semantically expressive as entire logics. We conjecture that this is representative of PDL-style, as well as closely related, logics.