Editing Property Specification Language (section)

=== LTL-style operators===

Below is a sample of some LTL-style operators of PSL.

Here {{mono|p}} and {{mono|q}} are any PSL formulas.
{| class="wikitable"
| {{code|always p}}
| property p holds on every time point
|-
| {{code|never p}}
| property p does not hold on any time point
|-
| {{code|eventually! p}}
| there exists a future time point where p holds 
|-
| {{code|next! p}}
| there exists a next time point, and p holds on this point 
|-
| {{code|next p}}
| if there exists a next time point, then p holds on this point 
|-
| {{code|next![n] p}}
| there exists an n-th time point, and p holds on this point 
|-
| {{code|next[n] p}}
| if there exists an n-th time point, then p holds on this point 
|-
| {{code|next_e![m..n] p}}
| there exists a time point, within m-th to n-th from the current where p holds. 
|-
| {{code|next_e[m..n] p}}
| if there exists at least n-th time points, then p holds on one of the m-th to n-th points. 
|-
| {{code|next_a![m..n] p}}
| there exists at least n more time points and p holds in all the time points between the m-th to the n-th, inclusive.
|-
| {{code|next_a[m..n] p}}
| p holds on all the next m-th through n-th time points, however many exist 
|-
| {{code|p until! q}}
| there exists a time point where q holds, and p hold up until that time point
|-
| {{code|p until q}}
| p holds up until a time point where q hold, if such exists
|-
| {{code|p until!_ q}}
| there exists a time point where q holds, and p holds up until that time point and in that time point
|-
| {{code|p until_ q}}
| p holds up until a time point where q holds, and in that time point, if such exists
|-
| {{code|p before! q}}
| p holds strictly before the time point where q holds, and p eventually holds
|-
| {{code|p before q}}
| p holds strictly before the time point where q holds, if p never holds, then neither does q
|-
| {{code|p before!_ q}}
| p holds before or at the same time point where q holds, and p eventually holds
|-
| {{code|p before_ q}}
| p holds before or at the same time point where q holds, if p never holds, then neither does q
|-
|}