Modal Logic Playground

rkirsling.github.io

82 points·jstrieb··3 comments

Modal logic was always a bit of a puzzle to me, but it does have importance in CS because of temporal logic, see [0], a kind of modal logic. I was introduced to it while doing research on the verification of total correctness of CSP style concurrent programs in the 1970's.

Verifying the correctness of concurrent systems is very difficult. My research was in a slightly different direction, but important progress in verification was being made in the 1970's by David Gries and Susan Owicki (see [1], an ACM award winning paper), and Leslie Lamport (see [2]) that made use of temporal logic. Temporal logic is used by Lamport's TLA+ today, see [3].

Further developments in temporal logic were made by Amir Pnueli as described in books and papers, see [4].

[0] https://en.wikipedia.org/wiki/Temporal_logic

[1] https://dl.acm.org/citation.cfm?doid=360051.360224

[2] https://dl.acm.org/citation.cfm?id=357178

[3] https://lamport.azurewebsites.net/pubs/lamport-actions.pdf

[4] https://en.wikipedia.org/wiki/Amir_Pnueli

It is possible that you are studying modal logic.

https://billwadge.wordpress.com/2015/09/30/i-deduce-you-are-...

Please consider the UX of your state toggles. The red/green states will be difficult for color-blind users to discern and, color aside, it's tough to tell which is the active state.

Reply on news.ycombinator.com