We survey one branch of algebraic logic, namely modal semirings. They provide compact algebraic definitions of actions, with choice \(+\) and sequential composition \(\cdot \)  , together with modal operators box and diamond, parametrised by actions, that allow reasoning about successors and predecessors of states/worlds. Particular instances are homogeneous binary relations or sets of finite and infinite non-empty traces under fusing concatenation. As main examples of applications we present obstacle analysis for geographic wayfinders, Hoare Logic, O’Hearn’s Incorrectness Logic, General Correctness Logic, as well as the temporal logic \(\textsf{CTL}^*\) and its sublogics \(\textsf{CTL}\) and \(\textsf{LTL}\) . We also give glimpses at Epistemic Logics of belief and knowledge, pointer structures plus Separation Logic and preference database queries. Finally, we briefly discuss some related algebraic approaches.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Some Uses of Modal Semirings

  • Bernhard Möller,
  • Jules Desharnais

摘要

We survey one branch of algebraic logic, namely modal semirings. They provide compact algebraic definitions of actions, with choice \(+\) and sequential composition \(\cdot \)  , together with modal operators box and diamond, parametrised by actions, that allow reasoning about successors and predecessors of states/worlds. Particular instances are homogeneous binary relations or sets of finite and infinite non-empty traces under fusing concatenation. As main examples of applications we present obstacle analysis for geographic wayfinders, Hoare Logic, O’Hearn’s Incorrectness Logic, General Correctness Logic, as well as the temporal logic \(\textsf{CTL}^*\) and its sublogics \(\textsf{CTL}\) and \(\textsf{LTL}\) . We also give glimpses at Epistemic Logics of belief and knowledge, pointer structures plus Separation Logic and preference database queries. Finally, we briefly discuss some related algebraic approaches.