Temporal Modal Logic

Temporal modal logic, simply stated, is the logic of possibility over time.

While temporal modal logic is already widely used in hardware and mission critical software to ensure that systems match their specifications, temporal modal logic is also well suited for specifying the formal aspects of human contractual agreements. Modality uses a temporal modal logic language called Modality to define and query constraints in user defined contracts over time.

The History of Modal Logic

First expressed by Aristotle as the logic of ‘possibility’ and ‘necessity’, modal logic itself took many centuries to develop. Leibniz recognized that ‘permitted’ (may) and ‘obligatory’ (must) were the legal equivalents of ‘possible’ and ‘necessary’ and began advocating for a calculus for universal communication and judgement. In 1879, Frege, inspired by Leibniz’s pursuit, was the first to publish such a formal calculus, calling it Conceptscript.

But when Bertrand Russell discovered Frege’s language had shipped with a catastrophic bug, the stage was set for a century of innovation in mathematics. Gödel asked what provability itself meant, and in the early 1930s used modal logic to formalize the concept and deliver his incompleteness theorems. With the birth of computers, came more bugs and wider question about the provability of programs. The Church-Turing thesis evinced that any computable problem could be performed on an abstract Turing machine. But such an abstraction came with a cost: Turing complete machines were also undecidable, and there was no way to anticipate if their programs would run to completion.

Jumping back to the 1910s, C. I. Lewis, became the first to classify modal logics by axiom, adopting the diamond symbol ◇ to mean ‘possible’ and the box symbol □ to mean ‘necessary’. In the 1950s, Arthur Prior, inspired by medieval logicians like William of Ockham, reintroduced time to modal logic. Prior expressed time as paths over possible worlds, founding what is now know as temporal modal logic. However, a semantics for these logics was still missing, but in 1959, Saul Kripke developed the accessibility relationship between possible worlds in a way that brought the work of Lewis and Prior naturally together.

By the late 1970s, all this pure theory was ready for practice and Amir Pneuli created the first programmable temporal modal logic to enable formal verification by computer, calling it Linear Temporal Logic (LTL). The need to work over branching-time lead Ed Clarke to develop Computational Tree Logic (CTL). While studying under Ed Clarke, Bud Mishra was the first to use temporal logic to identify a hardware bug, bringing widespread practical use to the field. Eventually, Dexter Kozen discovered that languages like CTL and LTL were both fragments of Dana Scott’s modal mu-calculus. As both temporal logic languages became widely used in industry, Moshe Vardi’s investigation into the robust decidability of modal logic solidified its use wherever tractability mattered.

Becoming the Logic of Modality

With the rise of distributed ledgers in the 2010s, Bud Mishra immediately recognized the need to incorporate formal verification and model checking. Bud initially envisioned an out-of-band form of model checking against what he called Kripke ledgers, and began discussing the concept with software architect, Foy Savas. After several years, Foy convinced Bud that an inversion of his ledger concept would better serve to formalize traditional contractual agreements. To do this, they defined a Kripke Machine able to enforce and extend a set of user-defined temporal modal constraints over time. Modality was subsequently designed as a logic language for the rights and obligations reified within a Kripke Machine. In 2022, Foy started work on a practical implementation of Modality as digital contract repositories.