Abstract: We introduce the formula-synthesis problem for Proposi-

tional Dynamic Logic with Shuffle (PDL || ). This prob-

lem, which generalises the model-checking problem again-

sts PDL || is the following: given a finite transition system

and a regular term-grammar that generates (possibly infinitely

many) PDL || formulas, find a formula generated by the gram-

mar that is true in the structure (or return that there is none).

We prove that the problem is undecidable in general, but add

certain restrictions on the input structure or on the input gram-

mar to yield decidability. In particular, we prove that (1) if the

grammar only generates formulas in PDL (without shuffle),

then the problem is EXPTIME-complete, and a further re-

striction to linear grammars is PSPACE-complete, and a fur-

ther restriction to non-recursive grammars is NP-complete,

and (2) if one restricts the input structure to have only simple

paths then the problem is in 2-EXPTIME. This work is moti-

vated by and opens up connections to other forms of synthe-

sis from hierarchical descriptions, including HTN problems

in Planning and Attack-tree Synthesis problems in Security.