| STL-based Guidance Signal Construction Rules for Secure CPS |
| φ1:=□[t1,t2]((xt(j)≥c1)∧¬(xt(j)≥c2)) | Stability (x(j),[t1,t2]) enforces physically valid ranges and prevents false high or low values outside feasible limits over time. |
| φ2:=□[t1,t2](¬((xt(j)≥c1)∧¬(xt(j+1)≥c2))) | Associativity (x(j),x(j+1),[t1,t2]) encapsulates the correlational associativity across features over time. |
| φ3:=¬(xt(j)≥c1)U[t1,t2](xt(j+1)≥c2) | Propagation (x(j),x(j+1),[t1,t2]) strengthens upstream and downstream system behavior between two sensor locations or across temporally related events. |
| φ4:=□[t1,t2](¬(∣xˉ[t−w1,t](j)−xˉ[t−w1−w2,t−w1](j)∣≥c1)) | Smoothness (x(j),[t1,t2],w1,w2) bounds the change in mean between adjacent windows of widths w1 and w2 , detecting persistent changes in feature behavior. |
| φ5:=□[t1,t2](¬((xt(j)≥c1)∧¬◊[d1,d2](xt(j+1)≥c2))) | Latency (x(j),x(j+1),[t1,t2],[d1,d2]) enforces that whenever feature x(j) reaches level c1 , feature x(j+1) reaches level c2 at some time within the future window [d1,d2] . |
| φ6:=◊[t1,t2]□[0,d]((xt(j)≥c1)∧¬(xt(j)≥c2)) | Recovery (x(j),[t1,t2],d) requires the feature to eventually enter and remain within a safe operational band for a duration of at least d time units. |