LDLf⁢formula ⁢φ ::=A∣¬φ∣φ1∧φ2∣⟨ρ⟩φ
Proposition ⁢ψ ::=LDLfformula w/o modality
Regular path ⁢ρ ::=ψ∣φ?∣ρ1+ρ2∣ρ1;ρ2∣ρ∗
Atomic proposition ⁢A ::=true∣false∣symbol