Quantile transformations

Path formula settings

Type of inner path formula: Finally B A Until B Globally B A Releases B Type of reward bound: Step/time bound Reward bound

Quantiles: Normal form syntax

Quantor	Probability bound	Formula
Universal Existential	>= p >  p <= p <  p	φ (F<=? B) ψ (F>=? B)	min/max trivial
A / E	< / > / =	F	T

Quantiles: Verbose syntax

min r max r	:	Pmin Pmax	[	φ (F<=? B) ψ (F>=? B)	]	>= p >  p <= p <  p
M		P

Equivalent quantiles (via transformations)

(Original) 0 Q0:
1 Q1:
2 Q2:
3 Q3:
Keep transformed quantiles frozen K

KEY = press key