A Curious Computer Science Problem

- -

I was discussing linguistics with my esteemed colleague and close friend Alex English earlier when I stumbled upon a very interesting computer science problem: the generation of grammatically-correct, semantically meaningful palindromes. The minute I typed my message about it I regretted it, because my immediate impression was that this is an extremely difficult problem.
We have to sort of reign it in just a little and make the problem more generic, too. So, let's say that we have one language P, a subset of a more generally-defined language comprised of only those recognizable phrases which are palindromes. It's fairly easy to arbitrarily generate phrases from a given grammar and lexicon but doing so in such a way that it remains a palindrome is somewhat challenging, but doing so in such a way that it remains syntactically correct is what we're interested in here.
Consider the following simple grammar:
S -> AA -> x A|  x
This grammar only generates strings of x's, so of course it only generates palindromes, and it can also generate arbitrarily-long strings. This is a patently ridiculous grammar but it does demonstrate one issue: how do you prove that your grammar even has a maximum-length palindrome? Consider the following grammar:
S -> AA -> x y A |  x y
That grammar produces an infinite number of phrases, none of them palindromes. How complicated is it to prove the existence or nonexistence of palindromes in a well-defined language?
Because it reminds me of some aspects of the Busy Beaver Problem, perhaps a version of the Busy Beaver Problem for push-down automata. If anyone's heard of it or better yet a proof of its complexity, let me know.
Thinking too much as always. Sleep tight, space cadets.