Modal μ-calculus on Min-plus Algebra N∞

スポンサーリンク

概要

• 論文の詳細を見る

• 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.

• Information and Media Technologies 編集運営会議の論文

著者

• Tanabe Yoshinori

  Graduate School Of Information Science And Technology The University Of Tokyo

• HAGIYA MASAMI

  Graduate School of Information Science and Technology, the University of Tokyo

• Tanabe Yoshinori

  Graduate School of Information Science and Technology, University of Tokyo

• Hagiya Masami

  Graduate School of Information Science and Technology, University of Tokyo

• Ikarashi Dai

  Graduate School of Information Science and Technology, University of Tokyo

• Nishizawa Koki

  Faculty of Environmental and Information Studies, Tottori University of Environmental Studies

関連論文

• Pre- and Post-Conditions Expressed in Variants of the Modal μ-Calculus
• A Retargetable Code Generator for the Generic Intermediate Language in COINS
• A Retargetable Code Generator for the Generic Intermediate Language in COINS
• Modal μ-calculus on Min-plus Algebra N∞

スポンサーリンク