temporal logic
This tool translates a temporal logic specification into a decomposed Value graph, which allows one to solve the optimal Value and policy for the given spec.
To write logic, compose the following symbols. Predicates can be any string.
Ffinally/eventually, to reach a stateUuntil||orGglobally/always, to avoid leaving a state&&and!notThe DVG is generated by first manipulating the temporal logic tree associated with the formula to make it amenable to Value decomposition algebra. Then the Value is defined over this structure and the rules applied, yielding a graph of max, min, negation, atomic Bellman Values (avoid, reach-avoid, reach-avoid-loop) and the predicates. This is equivalent to transforming the overall task Value into a coupled set of Values, each with a known Bellman equation.
Rendered specs. are stored in the url, so you can share a link directly to a graph.
eg.: F a && F b && G !w -> .../valtr/?spec=F-a-&&-F-b-&&-G-!w
dev note: Mechanics derive from code state in docs/py/valtr. Run
python scripts/build_web_bundle.py to update with current src/valtr code.