{"entities":{"Q557788":{"pageid":559555,"ns":120,"title":"Item:Q557788","lastrevid":77875655,"modified":"2026-05-06T10:15:34Z","type":"item","id":"Q557788","labels":{"en":{"language":"en","value":"An axiomatization of bisimulation quantifiers via the \\(\\mu\\)-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2184035"}},"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":"Q557788$1CBCFB99-6066-49A4-9C51-80ED9653E47A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"de36f0bbc535b4cc70237516db7f5fa705659567","datavalue":{"value":{"text":"An axiomatization of bisimulation quantifiers via the \\(\\mu\\)-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q557788$11F8B61B-88E1-4561-80EF-3C807B551A09","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"276f540d08be11d3453e89592160c451493448c3","datavalue":{"value":"1080.68078","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$DE35194B-B940-4669-93CC-6246113DBD1D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9bc4d377d3637058f1e83788786b9a25ae94a603","datavalue":{"value":{"entity-type":"item","numeric-id":481099,"id":"Q481099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$31F731A8-C908-4AB3-A428-EE87A2E01971","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a24a57d77aefd8460dbb03e9524615c44c518008","datavalue":{"value":{"entity-type":"item","numeric-id":392378,"id":"Q392378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$56664D1C-4E9C-45D3-9264-2FEEA0567DD9","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":"Q557788$A7B15E1A-53C6-4AC1-B0A2-B951B84C941C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3be35b99bc40d25914143aa31268a19fcdde1b9d","datavalue":{"value":{"time":"+2005-06-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q557788$AC2EFA8B-B33E-4A22-A4FE-39433FC25AB2","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5f168054a9fd0229b80887ada197e0eec14ff995","datavalue":{"value":"The idea of a bisimulation quantifier can be exemplified in the existential bisimulation quantifier \\(\\widetilde\\exists\\): a formula \\(\\widetilde\\exists X\\phi\\) holds in a model \\((M,V)\\) if and only if \\(\\phi(X)\\) holds in a model which is bisimilar to \\((M,V)\\) with respect to the language of \\(\\phi\\) minus the variable \\(X\\).  In the paper the authors establish a complete axiom system for Bisimulation Quantifiers Logic (BQL) and prove that the subsystem of BQL which contains Propositional Dynamic Logic (PDL) and the axioms and rules for bisimulation quantifiers is strong enough to deduce all theorems of \\(\\mu\\)-calculus translated into BQL. The authors prove the latter result using the completeness of the \\(\\mu\\)-calculus [see \\textit{I. Walukiewicz}, Inf. Comput. 157, No. 1--2, 142--182 (2000; Zbl 1046.68628)].  The exposition of logical techniques in the paper is perfectly flawless. However, there is a tiny misprint in the definition of a guarded formula on page 68. The definition says: ``A formula is called guarded if, for any bound occurrence of a variable \\(X\\), denoting by \\(\\sigma X\\) its fixpoint binding, then \\(X\\) is contained in a Cover \\dots''. The definition makes sense only if we remove ``then'' from the above cited statement. But it should be mentioned that technically this misprint does not imply any difficulties, and a reader familiar with [\\textit{D. Kozen}, Theor. Comput. Sci. 27, 333--354 (1983; Zbl 0553.03007)] should easily find a straightforward analogy between the definition of a guarded formula given by Kozen there and the definition used in this paper.","type":"string"},"datatype":"string"},"type":"statement","id":"Q557788$B86B9E33-1B1D-4453-B904-DF79E4195891","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"5c634a7a610dc4a60ec0b802b8dd89a79b8a3056","datavalue":{"value":{"entity-type":"item","numeric-id":588686,"id":"Q588686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$9F9451CF-CBF3-47E1-9E1E-337FFD120A3E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$D7A16956-0099-4E42-BF72-603391149F0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$EB08B9E5-6682-41BE-8E3A-E1B5C09CCB79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$B156E011-E4FB-4BB2-B55A-0B14BDB845D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25e5a5f23d3e2e2c05864da16eda493011c33276","datavalue":{"value":"03C80","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$FE45E8D4-E136-43FB-A9B2-8F1D9A2C4A1C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9740065bc182f800f579892b964be6b5c015d903","datavalue":{"value":"2184035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$15C6D6E0-74BB-4EC0-8DE9-565C2B0DA9E1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3e04a2b734a1cac93a9ddfefc5a4de51edbfaf1","datavalue":{"value":"bisimulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q557788$35697008-8D3F-4DE7-9FAD-C9CC613A8203","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a9a7b0cf17169865b15e8c9d7014c24bafb8410c","datavalue":{"value":"fixed points","type":"string"},"datatype":"string"},"type":"statement","id":"Q557788$2B21287F-FDAD-46E6-A48D-6FEB8F04BDE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1d13fe3141ed30017042d09d7bb940bc6ac1211a","datavalue":{"value":"bisimulation quantifiers","type":"string"},"datatype":"string"},"type":"statement","id":"Q557788$B789E49A-DAC2-48A3-A8E5-5C16B855676A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b7662493be8c807e4e49fd26f7b5c47a219f3196","datavalue":{"value":"\\(\\mu\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q557788$3F11B1BF-04E6-4044-BD4E-56A5A942C7AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"49321898cc9d8d40f95d16fb277499d0a0718cee","datavalue":{"value":"disjunctive formulas","type":"string"},"datatype":"string"},"type":"statement","id":"Q557788$29B2CC86-B1F3-475E-BB6A-7D7A33938831","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":"Q557788$76DE054F-10A5-4098-B7D6-B1BC21229626","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e823ad29652faa79b95f03813faf66ada187c678","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2004.10.040","type":"string"},"datatype":"url"},"type":"statement","id":"Q557788$2003EFF0-A836-46CB-A3CA-1A64332F4903","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2714937612f2b8d617e374a66298d66e45a96542","datavalue":{"value":"W2057583838","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$C440477F-234E-43ED-AD6A-6857D8A9D139","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"711e282bbd2865ebea7c8b287f5496055a3f9a3d","datavalue":{"value":{"entity-type":"item","numeric-id":4953222,"id":"Q4953222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$249581B1-3401-434C-AF81-C75667B8149F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"336b3ce90c4deb9f6127a52a430d218ebd8c1f8c","datavalue":{"value":{"entity-type":"item","numeric-id":4858826,"id":"Q4858826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$F0DDC141-969A-4C56-929C-318143EE3000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cec9ba6e99d0b988d6ab1227e6bdd591bb955386","datavalue":{"value":{"entity-type":"item","numeric-id":1577354,"id":"Q1577354"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$6F4FC4CC-664C-42E6-BB4F-812ECFF3A254","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b616d03b1219418af06ece48bd855e350c3cf3d4","datavalue":{"value":{"entity-type":"item","numeric-id":3569045,"id":"Q3569045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$E1840BA1-A4C8-4D5E-A67E-C185922C5D07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d0b3d39649082ff6de9169c6e51eb8e1d8d7a0b","datavalue":{"value":{"entity-type":"item","numeric-id":5385339,"id":"Q5385339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$C2F1F8DA-795E-44CD-8C97-3FCE13A866F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf5e0864e6808c186dd0092e7f961ddd594b13","datavalue":{"value":{"entity-type":"item","numeric-id":4008745,"id":"Q4008745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$22A984F8-061B-48BE-B17A-E273B171A8E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$4BBCF993-9B9F-4D6D-AF13-EEC49BC3D68D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08130677d950f0e9764f0a4bfbc64de21effa2bc","datavalue":{"value":{"entity-type":"item","numeric-id":4893140,"id":"Q4893140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$B3713EF1-3C8E-4609-9319-47735A583E26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"383a3ca7aae52562570b64d9d10b45f0e5fd4501","datavalue":{"value":{"entity-type":"item","numeric-id":4593948,"id":"Q4593948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$3B46F9E8-ACBC-4D7D-9964-CD2CCB01F690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53a659b2cbd537713eeed2150669304c9e3e0f0e","datavalue":{"value":{"entity-type":"item","numeric-id":1854336,"id":"Q1854336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q557788$C400BCB4-19F0-4051-AC87-B54536304634","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2f9b3a0e3fbdbb8f05935b166204ca1decc36afa","datavalue":{"value":"10.1016/J.TCS.2004.10.040","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q557788$FCAD96B9-AC12-4A7E-AEF2-3B816BE5B1EC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e590642790d6b9884ec6c573cef4baee6a1236b8","datavalue":{"value":{"entity-type":"item","numeric-id":5249664,"id":"Q5249664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec813d1001856c7289fe6cb300443d633d62ed62","datavalue":{"value":{"amount":"+0.8085425","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$6DACC067-FB38-442D-9939-D7FC58F2F5F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8360e23067f6d47764214a5f12daf6448a5281f8","datavalue":{"value":{"entity-type":"item","numeric-id":2506827,"id":"Q2506827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8aa17873937d7c659b0c07db2b48c16d30e86b6","datavalue":{"value":{"amount":"+0.80390584","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$188CCAA5-9F09-47D8-AD21-E684C76B4A02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e741cc559adec9531f855368e6140ea351d684b","datavalue":{"value":{"entity-type":"item","numeric-id":3509051,"id":"Q3509051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a337e5dbe7e0aef2dbc9efeb8e12f1dc231dfdc8","datavalue":{"value":{"amount":"+0.802189","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$0A857BAE-F201-4367-9D5D-C58EF043EA29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f54cb18e4020d77135267b262453765219c30e5","datavalue":{"value":{"entity-type":"item","numeric-id":4218096,"id":"Q4218096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44a1efba2b8bc17985e3b6f7ab53857f167b5257","datavalue":{"value":{"amount":"+0.7724167","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$B4066824-F853-4150-8E98-67DF0662C428","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48a5db2e7aff8de30376be70cb10f31c138b1d20","datavalue":{"value":{"entity-type":"item","numeric-id":4412841,"id":"Q4412841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4caa8757befd7ef45bb9265dc9566ad7ddc42900","datavalue":{"value":{"amount":"+0.7597625","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$30BFF63E-0B17-4320-98A4-811011AF8FA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9773ee3d70debc794eac4ab34c8a660087718bc5","datavalue":{"value":{"entity-type":"item","numeric-id":3591388,"id":"Q3591388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7cebc301cc3b6454ef9cb1a3f90963b74abdefe5","datavalue":{"value":{"amount":"+0.7567274","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$4C2CDC37-CD42-4695-A84B-669E5262D759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1edb9769746fb42a02708624bdf4fd2c496fcae","datavalue":{"value":{"entity-type":"item","numeric-id":3154151,"id":"Q3154151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a90ee47a203e8c5a84952f17b27029e6ea993f89","datavalue":{"value":{"amount":"+0.75655806","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$7AA9C553-C152-482C-97DF-E7E921F3A5A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f277dad969b10bf2e20a0cd1e2b00e0876a0cdb4","datavalue":{"value":{"entity-type":"item","numeric-id":4440830,"id":"Q4440830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd9c29ca070feef109f195155d13355d93aa5a46","datavalue":{"value":{"amount":"+0.7565358","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$4DBE9D9C-3CF5-4972-B3FC-D0DAC5B31950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"267fdc578b9b3d834449a779163a2a18ec5f6caf","datavalue":{"value":{"entity-type":"item","numeric-id":5412443,"id":"Q5412443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ae37269210e715c39fdd0ae044d878cc4deedf4c","datavalue":{"value":{"amount":"+0.7555678","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q557788$8AABEABA-FEEA-4267-B4E5-DE64D9EB96F5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An axiomatization of bisimulation quantifiers via the \\(\\mu\\)-calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_axiomatization_of_bisimulation_quantifiers_via_the_%5C(%5Cmu%5C)-calculus"}}}}}