Decidability and Undecidability Results of Modalμ-calculi with N∞ Semantics

概要

論文の詳細を見る
In our previous study, we defined the semantics of modalμ-calculus on minplus algebra N∞and developed a model-checking algorithm. N∞is the set of all natural numbers and infinity (∞), and has two operations min and plus. In the semantics, disjunctions are interpreted by min and conjunctions by plus. This semantics allows interesting properties of a Kripke structure, such as the shortest path to some state or the number of states that satisfy a specified condition, to be expressed using simple formulae. In this study, we investigate the satisfiability problem in N∞semantics and prove decidability and undecidability results. First, the problem is decidable if the logic does not contain the implication operator. We prove this result by defining a translation tr(ψ) of formulaψsuch that the satisfiability ofψin N∞semantics is equivalent to that of tr(ψ) in ordinary semantics. Second, the satisfiablity problem becomes undecidable if the logic contains the implication operator.
一般社団法人情報処理学会の論文
2009-11-20