On Frequency LTL in Probabilistic Systems

Vojtěch Forejt, Jan Krčál

We study frequency linear-time temporal logic (fLTL) which extends the linear-time temporal logic (LTL) with a path operator $G^p$ expressing that on a path, certain formula holds…