Skip to content

LDL Tools

Linear Dynamic Logic on finite traces (LDLf)1 is a recently-proposed extension of Linear Temporal Logic (LTL)2, a well-known propositional temporal logic introduced decades ago.
LDL Tools are a collection of small programs ranging from those for verifying LDLf formulas to those for processing smart contracts in an experimental LDLf-based DSL.

ldlsat

ldlsat is a SAT solver for LDLf.

dsl4sc

DSL4SC is a small experimental LDLf-based domain-specific language for defining correct event-processing systems in the sense that they are guaranteed, by construction, to meet their formally-specified requirements.

A set of tools are provided for DSL4SC processing, including rulessat for static formal verification and rules2scxml for translation from DSL4SC to SCXML.

scxmlrun

scxmlrun is a MQTT-enabled SCXML processor. Each SCXML process can send/receive events via MQTT.

References

  1. Giuseppe De Giacomo and Moshe Y. Vardi, "Linear Temporal Logic and Linear Dynamic Logic on Finite Traces". Proceedings of the 23rd international joint conference on Artificial Intelligence, AAAI Press, Aug 2013. ↩

  2. Amir Pnueli, "The temporal logic of programs". Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE Press, 1977. ↩