#kripke-structures

¶ I use modal logic at work every day, and the engineers around me have no idea it was philosophy

Every day, the engineers I work with write properties like "on every path, whenever a request is issued, a grant eventually follows". In our notation that's something like AG(request → AF grant): A for "on all paths", G for "always", F for…