[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Information and Media Technologies
Online ISSN : 1881-0896
ISSN-L : 1881-0896
Computing
Modal μ-calculus on Min-plus Algebra N
Dai IkarashiYoshinori TanabeKoki NishizawaMasami Hagiya
Author information
JOURNAL FREE ACCESS

2010 Volume 5 Issue 4 Pages 1178-1192

Details
Abstract

We have developed an interpretation of modal μ-calculus using min-plus algebra N, the set of all natural numbers and infinity ∞. Disjunctions are interpreted by min, and conjunctions by plus. This interpretation allows complex properties, such as the shortest path on a Kripke structure or the number of states that satisfy a specified condition, to be expressed with simple formulas. We defined the semantics of modal μ-calculus on min-plus algebra, and then described a model-checking algorithm for the semantics and its implementation. Although simple iterative computation of the least fixed-point generally does not terminate in N, due to abstraction, we made model-checking possible by reducing the least fixed-point computation to the greatest fixed-point computation. Finally, we discuss the relationship between our semantics and the theory of Kripke structures on complete Heyting algebra.

Content from these authors
© 2010 Japan Society for Software Science and Technology
Previous article Next article
feedback
Top