{"entities":{"Q1177939":{"pageid":1188688,"ns":120,"title":"Item:Q1177939","lastrevid":66508887,"modified":"2026-04-12T10:32:10Z","type":"item","id":"Q1177939","labels":{"en":{"language":"en","value":"Local model checking in the modal mu-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 22510"}},"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":"Q1177939$0998354A-238B-44B3-83F9-F8340CA4B856","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"343d1d7b52edfa7acbbcc78ec0e4bffed5f309f7","datavalue":{"value":{"text":"Local model checking in the modal mu-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1177939$6401C1C4-5B9A-4CBB-8C4C-AC0400988589","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a6567907a6a33dcd7653c232ca14012fdfcc2fa8","datavalue":{"value":"0745.03027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$CBAD086B-B79E-46E3-8546-66AFBD3DBE40","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e686d0b4e1d3281855db994cfdaaece00986dbcc","datavalue":{"value":"10.1016/0304-3975(90)90110-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$8AF29FBA-B615-4BDD-8DDB-3D5C8454EEC1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f5b17683dd2eedd3f1d821a1087aa218b2b31d17","datavalue":{"value":{"entity-type":"item","numeric-id":1160451,"id":"Q1160451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$DAEAC19B-69A5-4367-A257-D7B74E53ADCD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$2B97257B-E06A-4AAC-BFAF-1D190D340951","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1422b5e3113eee9dc98f0455d275631058399b8b","datavalue":{"value":{"time":"+1992-06-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1177939$EF795845-FB52-4AD5-B1B5-8F85E698FB12","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"508cd2d7ad6c60da1efa86fb8590529b9cc036b3","datavalue":{"value":"The modal mu-calculus introduced by Pratt and Kozen is an extension of dynamic logic towards temporal logic. Formulae of the mu-calculus when interpreted on labelled transition systems may be used for modelling concurrency. For a given finite model (transition system) the problem of satisfiability is solvable. The authors present a method which is a tableau system for testing whether or not a state \\(s\\) has the property expressed by a formula of mu-calculus in a finite model. A nice example of an application of the method is also provided (an analysis of Knuth's mutual exclusion algorithm).","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$424F7FF2-159A-4261-AA2B-C560A96FF471","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$2B9CB5DF-785C-4F6B-A96A-8F2705BC6F11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$F6B68611-D9E5-4AA3-81E4-736F6C9BBCD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$F34E2BDD-DE5A-471F-82D9-66744220D782","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$CC01473F-0E35-413D-9DBA-DA23EB6E5E53","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ced153f653ddbeef37b38d5f9da8973f03765f04","datavalue":{"value":"22510","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$B83EB695-414E-4578-A997-87D7DC349FA9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5dba8a14c151bd08273c5a04f1ad265d82751a87","datavalue":{"value":"CCS","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$D8CEB21B-1633-4DD0-9B2B-FC6C3E7565B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4421b72da5e69352497a79d6545f19cec17c3a4a","datavalue":{"value":"tableau method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$72CC4F8F-19C3-4EF0-BAD9-DC8A7DD9F222","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1079eb7de954d5da29808649edc4628f1387ad4f","datavalue":{"value":"satisfiability in finite models","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$6BB01CB3-8CAA-4181-BE1F-481C8B4D16AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b462f38abee80906c2d768906563204d6d43dfc5","datavalue":{"value":"modal mu-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$6C636EB6-F361-4353-BD37-E7EECA721C56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48a9d57224b4c90795ed16b4505d8da2503b1dae","datavalue":{"value":"dynamic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$A5DE423B-1B17-4BFA-96B3-0DCB7FFD9180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$24BDAE0A-3B58-4167-8560-FE9ACE1474D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d9c2e1f00facc619242af9af43a4aae006f38ad","datavalue":{"value":"transition systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$DDA8F9DF-FDAC-44FB-9083-040061FC2C7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"445a4fbc6b6bbba6e3c2169de8e334950d4f0826","datavalue":{"value":"concurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$9E0D5ECC-38FB-439A-BD39-073AB6AA3FCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51a5af629d6f91e707f4431c4bc3fa5154eab449","datavalue":{"value":"analysis of Knuth's mutual exclusion algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1177939$D783B948-5A93-43E5-952D-19F4337722DC","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"e797ff6dfa70600e9bb936f295518376bb337227","datavalue":{"value":{"entity-type":"item","numeric-id":794424,"id":"Q794424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$E3C3C13A-BBCD-462F-9F9D-090885536CA3","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":"Q1177939$4D27FBBD-AAA8-4149-A90A-1120D952673C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"362e3044d441e572f536dc5854cc309ba760962c","datavalue":{"value":"https://doi.org/10.1016/0304-3975(90)90110-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q1177939$CF9E8117-4A03-404F-905F-027D6BE0615A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a931c562dc997cd3f82ece142d854569998ac2c6","datavalue":{"value":"W1992582873","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1177939$0AF1AF71-DB8C-4599-9B0B-AEBF6E7ECCAB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c4261c45eb0bdc31b98abbe6dbdb3be8211dfa8","datavalue":{"value":{"entity-type":"item","numeric-id":1122572,"id":"Q1122572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$9F87C306-DD08-4644-B458-1518ADACF779","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c106f7cc54dee822f9d675291a8678b1806d2f8","datavalue":{"value":{"entity-type":"item","numeric-id":3719814,"id":"Q3719814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$8E4EFA4B-D2B3-4345-845A-755515021C90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf8ebc11e5152a7aaca233f3b6037de5f36fc738","datavalue":{"value":{"entity-type":"item","numeric-id":3766826,"id":"Q3766826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$8E8F31DD-92D7-47C8-A024-71878326A71F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"177c6c31d20ced5b129ead20e44a4131493dde0c","datavalue":{"value":{"entity-type":"item","numeric-id":911261,"id":"Q911261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$617242DC-4529-483E-86C1-CA5020F398B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f5a45904f81b6a39ede475e2e86ab18eb54c04e","datavalue":{"value":{"entity-type":"item","numeric-id":801893,"id":"Q801893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$E48E59C9-4391-4144-A496-B45D499B5865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd44e81af77baad910c4a8b87e7a0a1bfcec8eaa","datavalue":{"value":{"entity-type":"item","numeric-id":912592,"id":"Q912592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$597D8734-1CA0-466A-BFE4-C479750FF847","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"391e966cda7841966699f9d7a3bf9750dda40e97","datavalue":{"value":{"entity-type":"item","numeric-id":3992568,"id":"Q3992568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$63FFCB1C-721A-4340-8A52-D844366981C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a50bedffce465f6dca8b90f3cc27a20109b172b","datavalue":{"value":{"entity-type":"item","numeric-id":578896,"id":"Q578896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$F07C782F-741A-4981-BBAE-20B25F04B631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45280f113fe0216f2b7ecb89e3dff3eb55b2630c","datavalue":{"value":{"entity-type":"item","numeric-id":4733387,"id":"Q4733387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$F2D5F135-3793-4716-9532-5CB5DCEC577E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c647fa1d172318cd49d05d4eb4fca603299b18b0","datavalue":{"value":{"entity-type":"item","numeric-id":911263,"id":"Q911263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$55B014C8-9760-44B2-8C40-753AB93029BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1046b50af51c3932f3f883ecb7513f98f95e421c","datavalue":{"value":{"entity-type":"item","numeric-id":3033311,"id":"Q3033311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1177939$E7736211-9095-439E-A9B0-0274B1B7CD17","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd28868fb9e5281dec742e518f016b5bea1547d6","datavalue":{"value":{"entity-type":"item","numeric-id":1122572,"id":"Q1122572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df6f36acef0e518ad6070f9dad04d4f16a587a3e","datavalue":{"value":{"amount":"+0.852148175239563","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":"Q1177939$1B353FFF-5B1C-4B31-BAF8-636485F79383","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04513c0bdccc1d14a9c0a4e20e6bf9eab9493b6a","datavalue":{"value":{"entity-type":"item","numeric-id":1190489,"id":"Q1190489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0847ffd001f115f808c2cf83473b14c8ca144ea8","datavalue":{"value":{"amount":"+0.849278450012207","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":"Q1177939$F28CB608-58AC-4069-AAD5-3FB11B115B9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57df6c4616ac1c1e21409daa50b938d22cdce121","datavalue":{"value":{"entity-type":"item","numeric-id":1433941,"id":"Q1433941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6550b460202969196c0715b0dc5d69584ed1f77","datavalue":{"value":{"amount":"+0.8446235656738281","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":"Q1177939$BE7F90FB-9C7D-40FC-94A1-C8FDA63A6A2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14396cd9bd793a2ddf8fa5ff64e5c9589086b357","datavalue":{"value":{"entity-type":"item","numeric-id":5941205,"id":"Q5941205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72396323dbdd9c69282bf2abc5fbb38d76ed6cdc","datavalue":{"value":{"amount":"+0.8369631171226501","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":"Q1177939$8DC80D6E-3AF8-4798-9A8E-59F4807DDB94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"458bfc6f87b3dcd334c607afe3d711993c880250","datavalue":{"value":{"entity-type":"item","numeric-id":1176250,"id":"Q1176250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b634497c5589a70b6d1fe0fe9c906fdfacc2ba75","datavalue":{"value":{"amount":"+0.8368144035339355","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":"Q1177939$417BD262-5583-4588-A447-2EB44A51E14D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Local model checking in the modal mu-calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Local_model_checking_in_the_modal_mu-calculus"}}}}}