LDLf MODULO THEORIES
LDLf where the atoms are predicates over integers, not opaque letters.
The automaton construction doesn't care what atoms are, only that combinations of them can be checked for consistency. So each step carries linear integer predicates like {x > 100}, the satisfiable combinations become the alphabet (mintermization), and the contradictory ones are pruned away — every kept letter comes with a concrete witness value. Lydia builds the automaton and Z3 does the pruning, both compiled to WebAssembly — everything runs on your machine.
nothing translated yet
SYNTAX
Formulas are standard LDLf — tt, ff, end, last, modalities <ρ>φ and [ρ]φ, regular expressions with ; + * φ? — except that every atom is a predicate in braces: {x > 10}, {2*x + y <= 7}, {x != 0}. Combine them with ! & | outside the braces: {x > 0} & !{y = 2}.
Predicates are linear comparisons over integer variables (< <= > >= = !=). Syntactic variants of the same comparison — {x > 5}, {5 < x}, {x - 5 > 0} — are recognised as one atom. Each distinct atom doubles the alphabet, so at most eight are allowed.
Predicates only see the current step. That's a real boundary, not a missing feature: per-step predicates keep the construction a symbolic finite automaton and everything stays decidable, while predicates relating values across steps would make emptiness undecidable in general.