Content deleted Content added
Line 3:
Property Specification Language is a temporal logic extending [[Linear temporal logic]] with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of [[regular expressions]] and syntactic sugaring. It is widely used in the hardware design and verification industry, where [[formal verification]] tools (such as [[model checking]]) are used to prove or refute that a given PSL formula holds on a given design.
==
PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a {{color|orange|request}} should always eventually be {{color|orange|grant}} ed can be expressed by the PSL formula:
| |||