{"entities":{"Q1096609":{"pageid":1107361,"ns":120,"title":"Item:Q1096609","lastrevid":77752754,"modified":"2026-05-06T09:58:53Z","type":"item","id":"Q1096609","labels":{"en":{"language":"en","value":"Interpreting logics of knowledge in propositional dynamic logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4031636"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$58203BDD-F5FB-46B4-B33E-B914ED52BD4A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7a2298e2155a3a8a656cb873579c40bf5c7e926e","datavalue":{"value":{"text":"Interpreting logics of knowledge in propositional dynamic logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1096609$58FF3D83-013E-4C70-A138-5E8CB228738F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1a91fa85aac1c2934fe4e80c837101e1903c3e60","datavalue":{"value":"0634.03012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$B05B9176-2635-4746-AFC7-A11BA902DB19","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0f550b2085330400b5462c5c54d3b2a9689b524c","datavalue":{"value":"10.1016/0020-0190(87)90129-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$B306CDDA-F335-49A0-9C60-D206265D4FAD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9733af42aa0dabaad4ed03856f62da6a21001b10","datavalue":{"value":{"entity-type":"item","numeric-id":800080,"id":"Q800080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$A529F3E5-EAA3-4CE1-9EF2-81F91AF5546C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c9449ce466a2c684a15ed4352b5933311b5f46f1","datavalue":{"value":{"entity-type":"item","numeric-id":6482617,"id":"Q6482617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$A748C51A-D806-4405-9838-D618B2FC3CB3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$A3CE749C-4121-4141-A485-456D29271C59","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1096609$475ACFB6-02A3-4A9F-8A19-05B7859B1EA9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"50e99a72f49339764866725e8a4949c7f62b6827","datavalue":{"value":"A language of Propositional Temporal Knowledge Logic (PTKL) over a set of propositional symbols PROP and a finite set \\(PART=\\{1,...,n\\}\\) of participants with operators Y, G, U and \\(C_ H\\) is specified.    The semantics of PTKL is defined using a kind of Kripke model called a distributed protocol. The protocol is a tuple \\({\\mathcal P}=<n,Q,I,\\tau,\\pi >\\) for n participants, where Q is a set of local states, \\(I\\subseteq Q\\) n is a set of initial global states, \\(\\pi\\) : Q \\(n\\times PROP\\to \\{0,1\\}\\), \\(\\tau\\subseteq Q\\) \\(n\\times Q\\) n is the next move relation on global states, \\(\\tau\\) * is its reflexive transitive closure. Reachable global states are defined using I and \\(\\tau\\) *.    The satisfaction relation \\(<{\\mathcal P},q>\\vDash \\alpha\\) is defined for a protocol \\({\\mathcal P}\\), global state q and a PTKL formula \\(\\alpha\\). The definition covers the following intuition: \\(Y\\alpha\\) means that \\(\\alpha\\) holds at every next step (in branching time), \\(G\\alpha\\) means that \\(\\alpha\\) holds at all points in the future, \\(\\alpha\\) \\(U\\beta\\) means that \\(\\alpha\\) is true and remains true until \\(\\beta\\) becomes true, and \\(C_ H\\alpha\\) means that it is common knowledge among the members of a set H of participants that \\(\\alpha\\).    Main results of the paper are:    1. Interpretation of PTKL in Propositional Dynamic Logic with Converse (PDLC). Let \\(\\Phi\\) (PTKL), \\(\\Phi\\) (PDLC) be the sets of all formulas of PTKL, PDLC. There is an interpretation \\(f: \\Phi\\) (PTKL)\\(\\to \\Phi (PDLC)\\) such that for all \\(\\alpha\\), \\(\\alpha\\) is satisfiable iff f(\\(\\alpha)\\) is satisfiable. The mapping f is simultaneously log-space and O(n 2) time computable.    2. The satisfiability problem for PTKL is decidable in EXPTIME. (The satisfiability problem for PTKL is EXPTIME complete even with only one participant and no occurrences of \\(C_ H:\\) satisfiability for propositional logic of branching time remains EXPTIME complete with addition of any combination of knowledge operators.)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$2117653B-0088-4312-8AD1-A6EE540ECFA5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$32B0065B-F51C-4068-A774-6BB5AE5E0D42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$6393FF4B-2DFC-4D79-8003-9684817353B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"85991e41d5921c9f733fe99d088c198a921df086","datavalue":{"value":"68T99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$6839523C-ADB5-4B63-BBC2-DB7162D1779B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$0E5814CF-ACBD-45C0-9246-7E65866F2113","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$D1088ACD-FCAE-4972-8CB4-2725D36810F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$913B8B09-814F-4E3D-8900-7FBE0BF2F0DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d7656d1c841701431b0b3d99d23720089a267cbb","datavalue":{"value":"03D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$C0585AC8-5434-4ABC-BFB8-812FCADD3563","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bbd1c42625ba3e47c31ca4793732856794b60d27","datavalue":{"value":"4031636","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$5F595A1D-13B4-4A66-BB85-188F4859F611","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f82d9744537c8929843a9f698e900cd31ff81587","datavalue":{"value":"distributed systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$96389B87-60D3-49FA-9417-72EDC7CC33C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b153019f7309b569efc92e134ad8cb0a4c7a85e","datavalue":{"value":"Propositional Temporal Knowledge Logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$1C73D35B-CFCC-4C0F-8C38-6A51E449A748","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d15f9ea98cd57ce867704f3f24d98ceaefc8d87b","datavalue":{"value":"participants","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$30493D54-C70D-4B6F-8AE4-CD96DB4E5F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$41F464FC-5C13-481D-9414-D1895FBDA1BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3875c79fa835ac45a1818de05c1bd8b1020c938e","datavalue":{"value":"Kripke model","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$557AF8E8-F5E8-4259-96E0-421762356475","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a12e1e6638ea6782fccd19e219b598c9b7e87e13","datavalue":{"value":"distributed protocol","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$E4396CD4-66C3-4624-96E0-2B0F263AA0CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6721114f39173577694cf24a1b46849a7225c33","datavalue":{"value":"Propositional Dynamic Logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$472248A5-3444-466F-BC46-D684308A7744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"508d90ed2d0cb5ed3bb66db4c84128c9e2d80423","datavalue":{"value":"interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$EC6A1C89-3AC3-4818-A6AD-0E2176A4D814","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0b4d6e6089943a261128dec792d30fd4cdc9763","datavalue":{"value":"satisfiability problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$751A8519-5E92-4268-8AB3-F77EA85068BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae7015df820d54c37a280b2bc669339e589c19cd","datavalue":{"value":"branching time","type":"string"},"datatype":"string"},"type":"statement","id":"Q1096609$724F12AD-E437-4001-BB89-AD9A0E181CCB","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"f16d300f1af622676dccb372accc3bc0c9d577af","datavalue":{"value":{"entity-type":"item","numeric-id":588374,"id":"Q588374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$8FF94751-2B06-4E17-BA1A-3D76310D5FA5","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$B5378DFD-B7CF-42D6-A122-93B572BAC6C3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3908d7a35c9069fb81428b639452c7e21d97709a","datavalue":{"value":"https://doi.org/10.1016/0020-0190(87)90129-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q1096609$BF759D49-2495-4949-A847-D2028A9E2C99","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2b0affecbf8d3f406674463720e66d06c2bc809d","datavalue":{"value":"W2086062372","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1096609$C5B7EF9C-48D7-4671-AD87-D41370E35E94","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3cd835cd92b4ffb8a8dc9181c7068cd47877b025","datavalue":{"value":{"entity-type":"item","numeric-id":2265816,"id":"Q2265816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$201FF45C-8F1E-4E92-BD5B-EC9AEF74FFDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47c57a1bc98a9d819c8c4b25347f0c45d96256b1","datavalue":{"value":{"entity-type":"item","numeric-id":1258296,"id":"Q1258296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$695C3E4B-1B7F-4950-B20B-90B0982D0749","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07b4a5481d2ba20db96403c8a94b2eeed3801b42","datavalue":{"value":{"entity-type":"item","numeric-id":3477999,"id":"Q3477999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$45117350-5287-4690-8E5B-15021A593261","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5aacca35fa42fa3506555849bf0261505efea805","datavalue":{"value":{"entity-type":"item","numeric-id":3218103,"id":"Q3218103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$3243325B-ADA3-4F21-BC21-CB13518E30AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d998f10dbe733ce0c4fe3996b622c39d39adbcb","datavalue":{"value":{"entity-type":"item","numeric-id":3662639,"id":"Q3662639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1096609$18B044CC-E3F7-473C-821E-23DA51F022B8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d1ef50871cb0fb9f9eb1aa5a511fea903d35c3d","datavalue":{"value":{"entity-type":"item","numeric-id":1096972,"id":"Q1096972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c0e8b4c811f73e569baf9519f792c584d6c3fe4","datavalue":{"value":{"amount":"+0.8510287404060364","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1096609$1CE45F15-DD34-4F2B-B286-2D6B28566723","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e95ede2d91b2fe5458abd07dd292609f12e6de40","datavalue":{"value":{"entity-type":"item","numeric-id":3096821,"id":"Q3096821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"411003f7233d4708e3a18f54478df426d323ac26","datavalue":{"value":{"amount":"+0.7669302821159363","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1096609$6A75F4EE-FDB1-42A1-881E-CC3F309447FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fff0f5faa194e27cef46a6ed8dea84b9f46e90d","datavalue":{"value":{"entity-type":"item","numeric-id":4738471,"id":"Q4738471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5c4c8c3dad08c16cbbff679deb34b335344bb2b8","datavalue":{"value":{"amount":"+0.7664627432823181","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1096609$5207EB98-9733-4A46-95C0-BC0867918901","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"393c2d14d929b3d48c8354c84704c85ee9c9a234","datavalue":{"value":{"entity-type":"item","numeric-id":1193476,"id":"Q1193476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e783a770804218db014651322081fcd462daff6","datavalue":{"value":{"amount":"+0.7644173502922058","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1096609$54373FC3-B77B-4E91-8C5D-931666C173F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"997af5c7e27fcae73d7075d665cef4ca756586f4","datavalue":{"value":{"entity-type":"item","numeric-id":5434507,"id":"Q5434507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e783a770804218db014651322081fcd462daff6","datavalue":{"value":{"amount":"+0.7644173502922058","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1096609$3FFD456F-7CF0-406B-94DF-49205A1F58C1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interpreting logics of knowledge in propositional dynamic logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Interpreting_logics_of_knowledge_in_propositional_dynamic_logic"}}}}}