An input language for Maude-NPA. Rather than using the strand-based language used by Maude-NPA, the Maude-PSL uses a notation based on the Alice-Bob notation commonly seen in the literature. Maude-PSL endeavors to make Maude-NPA specifications more readable, easier to write, and less prone to error.