Proste wyrażenia logiczne w PSL-u (podobnie jak i w innych językach) pozwalają opisać stan ustalony układu. Sekwencje opisują zmiany zachodzące w układzie (np. przejście automatu ze stanu A do stanu B), więc mogą być w uproszczeniu traktowane jako wyrażenia logiczne z dodanym wymiarem czasu. Kombinacje wyrażeń logicznych i sekwencji tworzone przy użyciu operatorów temporalnych są nazywane właściwościami (ang. properties). Zarówno sekwencje, jak i właściwości mogą być w PSL-u zdefiniowane jako samodzielne obiekty z unikalną nazwą i zestawem parametrów.
Dyrektywy języka PSL używają właściwości zdefiniowane dla danego układu w procesie jego weryfikacji. Właściwości, które powinny być zawsze prawdziwe (asercje), są weryfikowane przy użyciu dyrektywy assert produkującej komunikaty błędu w przypadku niespełnienia właściwości. Właściwości opisujące pożądane wymuszenia dla danego układu są weryfikowane przy użyciu dyrektywy assume (ta dyrektywa jest dostępna podczas weryfikacji formalnej). W celu sprawdzenia czy dana właściwość była kiedykolwiek sprawdzana przez narzędzie weryfikacji można użyć dyrektywy cover;