日々の流転

λ. “Algebraic laws for nondeterminism and concurrency” by Matthew Hennessy and Robin Milner

先日、syd_syd さんに紹介してもらった Hennessy-Milner Logic の論文。ざっと読んだ。

プログラムを様相のラベルに使う様相論理は私もどこかで見たと思っていたのだけど、それは First Steps in Modal Logic の Chapter 13 SLL Logic で扱われていた Dynamic Logic だった。 ただ、この論文の p.141 には以下のようにあるので、ちょっと違うのかな。

Although we do not here develop L into a logic for reasoning about programs, it is worth noting that as a language it is endogenous by Pnueli's classification [8]. This means that a formula states something about the `world' of a single program, in contrast to exogenous logics such as Dynamic Logic [9] where parts of programs may be constituents of formulas.

【2008-03-17】 Dynamic logic (modal logic) - Wikipedia, the free encyclopedia を読んでも、この違いをどう考えれば良いのかわからない…… orz