{"entities":{"Q1122572":{"pageid":1133321,"ns":120,"title":"Item:Q1122572","lastrevid":49289368,"modified":"2026-01-06T22:08:02Z","type":"item","id":"Q1122572","labels":{"en":{"language":"en","value":"Tableau-based model checking in the propositional mu-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4106831"}},"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":"Q1122572$9E8B9C8A-F5DA-4E5A-81C8-CDD561A5CECC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"45982764f6c0d2f93431e0883f2af59750c576be","datavalue":{"value":{"text":"Tableau-based model checking in the propositional mu-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1122572$37E0AF3A-F44E-4A66-91DD-9945F29D260D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0b6e3bb5913177c94706db2b1382459694cdb2b0","datavalue":{"value":"0676.03033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122572$6FEB39F5-95D5-4E7D-8C68-4185E503DA6E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4b42e0f25d2b7f93d95f8b0e64800df406e5fc4c","datavalue":{"value":"10.1007/BF00264284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122572$8DDAD3DA-A2BD-4D50-9129-E57DA7FC49DF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3f68f16bc588a14cf8a1841c177a5c562620a294","datavalue":{"value":{"entity-type":"item","numeric-id":234678,"id":"Q234678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122572$2D880314-6AC4-49F1-B2E1-E25363EDB622","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1122572$67060B51-12A8-4126-9ED8-F3648B3F4EA9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-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":"Q1122572$E266D1BB-76CA-441C-BACF-4B7DC1E6BA06","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"88616e7bbaf678189af22c52bae1d2428f90d784","datavalue":{"value":"This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122572$96505DCE-3312-49B7-9072-462483F459BC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122572$64B1860E-2503-4D6A-8436-B6EB737E6F93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122572$671DD610-DD37-4F4F-ABBA-D0046DFFD319","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e200485a057cbd2e4b8d12cce47067de41a8b649","datavalue":{"value":"4106831","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122572$746AF6DD-24E8-431E-868A-36D54DA02D1E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e85ea4e2888aedb7454a9a43dfeb1c1ec5d7f5ff","datavalue":{"value":"automated analysis of concurrent systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122572$1DAF3503-C5B9-4EC7-A905-0EAE1080CA35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a2003496f989f52f10d8eb5f5940609debfc871","datavalue":{"value":"finite-state systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122572$92BCFD3A-4329-42AD-B021-935D8FAA277B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2fd9f1f90d4d1cc7b80e544082d1978afe9f5d03","datavalue":{"value":"propositional mu-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122572$32C10B41-0DB6-48E5-BAFE-45DCAF350CE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bddd2a9f9618fb33d2bdc2d304716d77d2e2b670","datavalue":{"value":"tableau-based proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1122572$100706B0-E060-4BA8-895F-A1367A4F2393","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":"Q1122572$1B5427E6-F1C4-4000-82C0-CD8CA397EE97","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"57c9f75b52dcd291c28a0f4252fd4b03c6420f6a","datavalue":{"value":"https://doi.org/10.1007/bf00264284","type":"string"},"datatype":"url"},"type":"statement","id":"Q1122572$AFC526FA-8C3C-414D-9A98-0CB68F66710C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fb66b4c6a5a547eb5875e3b10cfa9a471a575477","datavalue":{"value":"W2057260173","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1122572$D743D315-B3A3-4A28-BAA8-44BCF55011A2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a9e8a2d94c894dc320f2d03a35ec3c28526ed1e8","datavalue":{"value":{"entity-type":"item","numeric-id":4818827,"id":"Q4818827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb8da47004d15bcb232ee45e6412f0aa446a6c96","datavalue":{"value":{"amount":"+0.8529888391494751","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":"Q1122572$78CAB4E4-10D7-48C4-AA9B-9744A0BFDA08","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":"81beedf9816d2741380cc352941f5931afb014f1","datavalue":{"value":{"amount":"+0.8527064323425293","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":"Q1122572$F8E7F54D-D9AD-4C1F-B396-460C2F3E4D92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8eb6256bad2c2f5fad3d464a16392ea9b77d5c24","datavalue":{"value":{"entity-type":"item","numeric-id":1177939,"id":"Q1177939"},"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":"Q1122572$479E3983-6A08-401C-B70C-B59CED107C7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"959d3e2d9fee2bd612a3fb8d6b0bf11e9ec36177","datavalue":{"value":{"entity-type":"item","numeric-id":703588,"id":"Q703588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c3673b0fed49cb1bd266ea194b9dd8cd54e7972d","datavalue":{"value":{"amount":"+0.8458642959594727","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":"Q1122572$BF7640B9-9673-4CF9-B462-FE4731359C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b6a1754e9f24f53d0ad889d0482f26317c0f3b22","datavalue":{"value":{"entity-type":"item","numeric-id":4501131,"id":"Q4501131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da0eb5ab1444012071b2f25b001f6261e9adbe28","datavalue":{"value":{"amount":"+0.830643355846405","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":"Q1122572$71CEF959-0498-4C02-A3CF-2D2FD81FBC73","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1122572","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1122572"}}}}}