LDLf
Linear Dynamic Logic on finite traces, translated to a deterministic finite automaton.
LDLf takes its syntax from propositional dynamic logic but reads it over finite traces, which buys you full monadic second-order expressiveness — strictly more than LTLf. Every formula still has an equivalent DFA. This runs Lydia compiled to WebAssembly, so the translation happens on your machine.
⌘↵
EXAMPLES
AUTOMATON
nothing translated yet
SYNTAX
Formulas are tt, ff, end, last, or a modality over a regular expression: <ρ>φ and [ρ]φ, combined with ! & | -> <->.
Regular expressions are propositional steps (a, !a & b, true) composed with ; (sequence), + (union), * (star), and φ? (test). Note that a bare proposition is a step, not a formula — “eventually b” is <true*;b>end, not <true*>b.
∎