WEKO3
アイテム
Decidability and Undecidability Results of Modalμ-calculi with N∞ Semantics
https://ipsj.ixsq.nii.ac.jp/records/67109
https://ipsj.ixsq.nii.ac.jp/records/67109d192517f-687e-4844-bb5f-bf9ad33974f3
名前 / ファイル | ライセンス | アクション |
---|---|---|
![]() |
Copyright (c) 2009 by the Information Processing Society of Japan
|
|
オープンアクセス |
Item type | Trans(1) | |||||||
---|---|---|---|---|---|---|---|---|
公開日 | 2009-11-20 | |||||||
タイトル | ||||||||
タイトル | Decidability and Undecidability Results of Modalμ-calculi with N∞ Semantics | |||||||
タイトル | ||||||||
言語 | en | |||||||
タイトル | Decidability and Undecidability Results of Modalμ-calculi with N∞ Semantics | |||||||
言語 | ||||||||
言語 | eng | |||||||
キーワード | ||||||||
主題Scheme | Other | |||||||
主題 | 発表概要 | |||||||
資源タイプ | ||||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
資源タイプ | journal article | |||||||
著者所属 | ||||||||
Ecole Normale Superieure | ||||||||
著者所属 | ||||||||
The University of Tokyo | ||||||||
著者所属 | ||||||||
The University of Tokyo | ||||||||
著者所属(英) | ||||||||
en | ||||||||
Ecole Normale Superieure | ||||||||
著者所属(英) | ||||||||
en | ||||||||
The University of Tokyo | ||||||||
著者所属(英) | ||||||||
en | ||||||||
The University of Tokyo | ||||||||
著者名 |
Alexis, Goyet
× Alexis, Goyet
|
|||||||
著者名(英) |
Alexis, Goyet
× Alexis, Goyet
|
|||||||
論文抄録 | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 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. | |||||||
論文抄録(英) | ||||||||
内容記述タイプ | Other | |||||||
内容記述 | 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. | |||||||
書誌レコードID | ||||||||
収録物識別子タイプ | NCID | |||||||
収録物識別子 | AA11464814 | |||||||
書誌情報 |
情報処理学会論文誌プログラミング(PRO) 巻 2, 号 5, p. 46-46, 発行日 2009-11-20 |
|||||||
ISSN | ||||||||
収録物識別子タイプ | ISSN | |||||||
収録物識別子 | 1882-7802 | |||||||
出版者 | ||||||||
言語 | ja | |||||||
出版者 | 情報処理学会 |