首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:min-plus代数N上の様相μ計算
  • 本地全文:下载
  • 作者:五十嵐 大 ; 田辺 良則 ; 西澤 弘毅
  • 期刊名称:コンピュータ ソフトウェア
  • 印刷版ISSN:0289-6540
  • 出版年度:2010
  • 卷号:27
  • 期号:3
  • 页码:3_99-3_113
  • DOI:10.11309/jssst.27.3_99
  • 出版社:Japan Society for Software Science and Technology
  • 摘要:

    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.

国家哲学社会科学文献中心版权所有