2. Writing Specifications for PyCASSE¶
PyCASSE supports specifications written in Signal Temporal Logic (STL) and Stochastic Temporal Logic (StSTL).
2.1. PyCASSE Syntax¶
An STL [Maler04] or an StSTL [Nuzzo19] formula can be written in PyCASSE using the following PyCASSE syntax in Backus-Naur form:
<boolean> ::= "TRUE" | "FALSE"
<digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
<letter> ::= "A" | "B" | "C" | "D" | "E" | "H" | "I" | "J" | "K" | "L" | "M"
| "N" | "O" | "Q" | "R" | "S" | "T" | "V" | "W" | "X" | "Y" | "Z"
| "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" | "k" | "l" | "m"
| "n" | "o" | "p" | "q" | "r" | "s" | "t" | "u" | "v" | "w" | "x" | "y" | "z"
<integer> ::= <digit> | <digit> <integer>
<interval> ::= "[" <integer> "," <integer> "]"
<variable> ::= <letter> | <letter> <variable> | <variable> <integer>
<expression> ::= <integer> | <variable> | <integer> "*" <variable>
| <expression> "+" <expression>
| <expression> "-" <expression>
<inequality> ::= <expression> "<" <expression>
| <expression> ">" <expression>
| <expression> "<=" <expression>
| <expression> "=>" <expression>
| <expression> "==" <expression>
<predicate> ::= <boolean> | <inequality> | "P(" <inequality> ") => 0." <integer>
<formula> ::= "(" <predicate> ")"
| "(!" <formula> ")"
| "(" <formula> " & " <formula> ")"
| "(" <formula> " | " <formula> ")"
| "(" <formula> " -> " <formula> ")"
| "(G" <interval> " " <formula> ")"
| "(F" <interval> " " <formula> ")"
| "(" <formula> " U" <interval> " " <formula> ")"
For example, ‘Globally from time step \(0\) to \(3\), \(2x \geq 3\) implies eventually from time step \(4\) to \(5\), the probability of \(5 \leq y\) larger than or equal to \(0.95\)’ can be written as an StSTL formula: \(\mathbf{G}_{[0,3]}(x \geq 3) \rightarrow \mathbf{F}_{[4,5]}(P\{ 5 \leq y \} \geq 0.95)\) and can be written as a formula in PySTL:
((G[0,3] (2*x => 3)) -> (F[4,5] (P(5 <= y) => 0.95)))