syntactic characterization of PSL subclasses
I think {r_F}
and !{r_F}
both belong to the φ_F
fragment. I'd also add {r_F}[]->φ_F
and {r_F}<>->φ_F
.
I think {r_F}
and !{r_F}
both belong to the φ_F
fragment. I'd also add {r_F}[]->φ_F
and {r_F}<>->φ_F
.