Upgrade to Pro — share decks privately, control downloads, hide ads and more …

様相μ計算による計算論的な民主主義の健全性の評価 ~自律分散組織(DAO)による政体の超越性に...

sgtn
September 13, 2022

様相μ計算による計算論的な民主主義の健全性の評価 ~自律分散組織(DAO)による政体の超越性に向けて~ The theory of democraticity evaluation via modal mu-calculus for suggesting the supremacy of DAO for Nations.

sgtn

September 13, 2022
Tweet

More Decks by sgtn

Other Decks in Research

Transcript

  1. 
 FIT2022 બ঑ηογϣϯ ڭҭɾਓจՊֶ CN-002
 
 ༷૬μܭࢉʹΑΔܭࢉ࿦తͳຽओओٛͷ݈શੑͷධՁ ʙཱࣗ෼ࢄ૊৫(DAO)ʹΑΔ੓ମͷ௒ӽੑʹ޲͚ͯʙ མ߹বޛ† ,

    ඌܗֶ࢜‡ , ࢁాݑ࢚† , ହ݈ؒ࢘† , ୩ా७† , ٶ੢ࣣւ† Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved † େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ εϚʔτίϯτϥΫτ׆༻ڞಉݚڀߨ࠲ ‡ ߹ಉձࣾsg
  2. ख๏ Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved

    4 FIT2022 બ঑ηογϣϯ GSM (Government State Machine / ੓෎ͷঢ়ଶػց) άϩʔόϧεςʔτ Committee Proposal ߦ੓A_i (e.g., ࢘๏, ܉) Committee proposal assignees treasury member committee substate budget member committee
  3. ख๏ Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved

    5 FIT2022 બ঑ηογϣϯ GSM (Government State Machine / ੓෎ͷঢ়ଶػց) ৼΔ෣͍ͷఆٛ : act, proposal ߏ଄ͷఆٛ : state, subState, committee Inductiveએݴ Recordએݴ
  4. ख๏ LTSͱ͸ɺΞΫγϣϯʹΑΓϥϕϧ෇͚͞Εͨɺঢ়ଶભҠΛҙຯ͢Δೋ߲ؔ܎ͷ ू߹Ͱ͋ΔɻΞΫγϣϯͷू߹Aͱঢ়ଶͷू߹S͕༩͑ΒΕͨ࣌ɺˠ ⊆ S × A × SͱͳΔू߹ˠΛɺLTSͱ͢Δɻ͢ͳΘͪɺa ∈

    A ͱ s,s’ ∈ Sʹରͯ͠ɺ(s, a, s’) ∈ ˠ ͱͳΔ࣌ɺঢ়ଶs͕ΞΫγϣϯaʹΑΓঢ়ଶs’ʹભҠ͠ಘΔࣄΛҙຯ͢Δɻ Ҏ ԼɺPDLͱCTLʹ͓͚Δঢ়ଶભҠ͸ɺLTSʹΑͬͯఆٛ͞Ε͍ͯΔ΋ͷͱ͢Δɻ Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved 7 FIT2022 બ঑ηογϣϯ LTSʢLabeled Transition Systemʣ × = cartessian product (௚ੵ) s ˠ s' a
  5. ख๏ PDLͱ͸ɺҰൠతͳ໋୊࿦ཧʹඞવੑɾՄೳੑΛҙຯ͢ΔԋࢉࢠΛՃ͑ͨ࿦ཧମܥͰ͋ΔɻΞ Ϋγϣϯa ∈ Aͱ࿦ཧ໋୊Pʹରͯ͠ɺ[a]Pͱ<a>P͕ͦΕͧΕඞવੑͱՄೳੑΛද͢ɻ໋֤୊ ͷ௚ײతͳҙຯ͸ҎԼͷ௨ΓͰ͋Δɻ ঢ়ଶsʹ͓͍ͯ[a]P͕੒Γཱͭࣄ͸ɺ s͔ΒaΛߦ࢖ͨ͠ޙͷ͍͔ͳΔঢ়ଶͰ΋P͕੒ΓཱͭࣄΛҙຯ͢Δɻ (e.g., That

    road is dry. -> [It rains.] That road is wet.) ঢ়ଶsʹ͓͍ͯ<a>P͕੒Γཱͭࣄ͸ɺ s͔ΒaΛߦ࢖ͨ͠ޙͰ΋P͕੒Γཱͭঢ়ଶ͕ଘࡏ͢Δɻ Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved 8 FIT2022 બ঑ηογϣϯ PDLʢPropositional Dynamic Logicʣ s ˠ s' [a] s ˠ s' <a> s' likely P s' should P
  6. ख๏ Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved

    10 FIT2022 બ঑ηογϣϯ CTLʢComputational Tree Logicʣ ࡞༻ૉͷ࠷খηοτͱॻ͖׵͑ Aφ = ͢΂ͯͷܦ࿏ʹ͍ͭͯ Eφ = গͳ͘ͱ΋1ͭͷܦ࿏͕ଘࡏ͠ Gφ = ͦͷޙͷશͯͷܦ࿏Ͱৗʹਅ Fφ = ͦͷޙͷܦ࿏ͷ͍ͣΕ͔ͷ࣌఺Ͱਅ Xφ = ࣍ͷঢ়ଶͰਅ φUψ = φ͸ɺ͋Δ࣌఺Ͱψ͕ਅͱͳΔ·Ͱ ͸ਅ
  7. Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved 11

    FIT2022 બ঑ηογϣϯ Definition soundness := forall s m adm, s |= NotDictatorial m adm. Definition NotDictatorial : form := assigned → AF (¬ undismissable). Definition undismissable : form := proposed → [deliberate]assigned. Definition deliberate : act := AsubDeliberate adm. Variable m : citizen. Variable adm : admin. Inductive var := | isAssigned : adm -> m -> var | isProposed : adm -> proposal -> var $5- 1%- ඁ໔ఏҊ͕͋Δͱ͖ɺݸผߦ੓Ͱख़ٞͯ͠ɺৗʹBTTJHOFEঢ়ଶ ͜ͷ$PRϥΠϒϥϦԽ͞Εͨ׆ ੑʹ͍ۙ࿦ཧΛѻ͑Ε͹ʮඁ໔ Ͱ͖ͳ͍ࢢຽʯͷ݁Ռ੔߹తෆଘ ࡏΛূ໌Ͱ͖Δ ݁Ռ ݸผߦ੓Ͱͷख़ٞͷ࣮ߦ ͢΂ͯͷߦ੓ͱࢢຽ΁ద༻ ৼΔ෣͍ͱߏ଄ͷ্ʹ໋୊Λఆٛ
  8. ݁Ռ Copyright© 2022 େࡕେֶ େֶӃ ৘ใՊֶݚڀՊ ৘ใ਺ཧֶઐ߈ All Rights Reserved

    12 FIT2022 બ঑ηογϣϯ Definition proposed : form := Var (isProposed adm (PdismissalMember adm m)). Definition assigned : form := (Var (isAssigned adm m)). ඁ໔ఏҊ ݕࠪର৅ͷࢢຽ͕ߦ੓ʹॴଐ͍ͯ͠Δ͜ͱ