{"entities":{"Q414899":{"pageid":416666,"ns":120,"title":"Item:Q414899","lastrevid":61672638,"modified":"2026-04-11T00:53:03Z","type":"item","id":"Q414899","labels":{"en":{"language":"en","value":"Multi-valued model checking games"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6033502"}},"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":"Q414899$0FA6C8FD-291E-4756-AC56-9B73FA79AAA5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"401a5468ca6a8c0fa6535ee928d49a1a724e87bf","datavalue":{"value":{"text":"Multi-valued model checking games","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q414899$C9934385-10C4-4BF2-83E0-7359E2F15693","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c4e3fad4800f0ad0560cd7aa3d907caa5e3ed95c","datavalue":{"value":"1257.68105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q414899$8B68AE28-9F23-4123-AF7C-6466C5DA30A2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cec177c60e5a5e06c4135c2d656205cdaac4e3ae","datavalue":{"value":{"entity-type":"item","numeric-id":259064,"id":"Q259064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$42DEC7F5-EEB0-42AE-9A35-A5CB31F84F98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dde9477c31764f7e982fa5c7962174291d7bf7fb","datavalue":{"value":{"entity-type":"item","numeric-id":259063,"id":"Q259063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$34B05654-6C18-4C1E-9332-4A7D96E157B6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3340243f57e05f2265c56423c388055a14b114fa","datavalue":{"value":{"entity-type":"item","numeric-id":107189,"id":"Q107189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$A499D445-9639-423C-87B2-1B35EB984004","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ebad7c55eb31a5728be157b82e80bb61556d824d","datavalue":{"value":{"time":"+2012-05-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q414899$1C590397-72F6-49C0-9F9E-CBE0729EE1A5","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"3b235b2ffc61208ddb9148c8c34fce39c3418332","datavalue":{"value":{"entity-type":"item","numeric-id":436314,"id":"Q436314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$0B4CC302-C57F-49A6-9A15-99B7C8EEB303","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q414899$14934FDF-B4CC-43F6-AD71-2D763F7DEADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d5c83f057600e5614b7fec59c8e4ac61cb41ba8d","datavalue":{"value":"91A80","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q414899$1C0B5C3C-671E-4813-8A88-3371B8CBFEA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q414899$2A6DDD21-9F12-4FE4-8685-73025AA63CE5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e26b840f16677582a8b890ffe9312f1d409cc1b4","datavalue":{"value":"6033502","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q414899$D0F28F34-ED53-4C96-933C-F3DA88A47EDE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q414899$2CFC3A0A-6DC0-4003-A267-315CAFAF2E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7aa3fdbdf3b7584bcd007098b5e184978502a1cf","datavalue":{"value":"mu-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q414899$71EC85ED-1860-465D-9360-C9FFBA73B9A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9e1dfeb3e80a9aec5df5036ceafe3264f0d82f0a","datavalue":{"value":"multi-valued semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q414899$FB6EFDB5-DA94-4078-82C1-0826F98FF415","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a08d7bd46c1f4e77be42a85ccd5869f9b0abf724","datavalue":{"value":"game-based setting","type":"string"},"datatype":"string"},"type":"statement","id":"Q414899$7D96D830-8264-44F0-8690-2EE6B7F68796","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":"Q414899$E876E14E-1CC1-40D5-BF79-41838F8F30FA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0d46df230cfd5da6b4d3ae1d22073cae5921d365","datavalue":{"value":"https://doi.org/10.1016/j.jcss.2011.05.003","type":"string"},"datatype":"url"},"type":"statement","id":"Q414899$E76E0601-6270-40D4-B376-0E360E3B3D4D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c85a6eaf35c1f928e9fa98eaa9d658cdbc4812bb","datavalue":{"value":"W2037024461","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q414899$F9C55B82-D417-43D8-A226-63EFB9066A0B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2297089ec0d4cef71c8ea1149f99b461e26387b2","datavalue":{"value":{"entity-type":"item","numeric-id":5491877,"id":"Q5491877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$9C1F640E-A690-4685-80B3-B2FE9902A48A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1cb46b665c4d01cdd72f034cac6c7dac8481fe1b","datavalue":{"value":{"entity-type":"item","numeric-id":4818796,"id":"Q4818796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$5B5C35AC-6C0E-4C80-AB86-B7979D6AD7DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7028552be8657cea7c6ef870efa608f422e607c","datavalue":{"value":{"entity-type":"item","numeric-id":5277790,"id":"Q5277790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$C1374BA7-306F-40BD-AEE5-DCE6F750B81C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89b378602d866701dabdb7cf5317c937b47e2621","datavalue":{"value":{"entity-type":"item","numeric-id":5711492,"id":"Q5711492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$0D76A5EF-BD43-439A-B2F4-57D5A52826A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43ded28dfcddfc12e7756640329f103bf1a26e17","datavalue":{"value":{"entity-type":"item","numeric-id":2754106,"id":"Q2754106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$D3E19465-CAE1-4E11-B0CA-0F32F7AA05CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06af39ba7611ce840efed59d15b9062e58635f61","datavalue":{"value":{"entity-type":"item","numeric-id":4804892,"id":"Q4804892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$7CD68DCE-500C-4A4A-8C87-A83246DD80B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c36da588071d067059823d7e571d291ad38c486d","datavalue":{"value":{"entity-type":"item","numeric-id":5900571,"id":"Q5900571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$7FB6E7FD-70B6-4E14-9D5D-A79A95C30E36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06f6d90e3236a929532aa1862e383e0fb9e24ea6","datavalue":{"value":{"entity-type":"item","numeric-id":5466469,"id":"Q5466469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$640BAC59-B73D-4B1C-85F1-AFCA33D0886D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"645c248b799110e0295b4065710f8300f24dbbaf","datavalue":{"value":{"entity-type":"item","numeric-id":4818743,"id":"Q4818743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$0EED62B9-3722-423B-8F0A-0F082BE4E753","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"481547f60ed568130e5c759ceeacc52cf0d1c02c","datavalue":{"value":{"entity-type":"item","numeric-id":5900684,"id":"Q5900684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$67FEE70E-202D-498E-9F37-BEAC8E554762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a6d2db3368a3e599316e7e7ac61a76cea0dd8c2","datavalue":{"value":{"entity-type":"item","numeric-id":4531751,"id":"Q4531751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$292A2411-768F-4ED8-9DF0-DF61DF3C517A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c5a4ef9c2d07db759cae7360b9f45883aa9ce65","datavalue":{"value":{"entity-type":"item","numeric-id":862857,"id":"Q862857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$A58DF4A2-2A29-4E0D-A6D0-A57157CFA5CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa4614c3d7786f0db16d6ca3adbca9b075e1b1ff","datavalue":{"value":{"entity-type":"item","numeric-id":1177939,"id":"Q1177939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$C7CC542A-48A0-4306-B9B3-0C0F10863719","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":"Q414899$4927B897-95F0-4278-A66A-0E74DE19D24C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc6ba7cd90791981ef59c6a62e83bd3990922df5","datavalue":{"value":{"entity-type":"item","numeric-id":4938419,"id":"Q4938419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$91F49AF9-0C9A-4731-95BC-EAE4EDC02063","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":"Q414899$2081DB87-C7A0-4D63-B0CD-0DA1D9115281","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08bfba2a3e8a1f2289573f123198c5b87769df67","datavalue":{"value":{"entity-type":"item","numeric-id":5176026,"id":"Q5176026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$70E0C5FC-7958-4E65-B312-3F13AA0884DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d4dd4faeed82b17a31b15b4f4a630199ca52442","datavalue":{"value":{"entity-type":"item","numeric-id":4692885,"id":"Q4692885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$1A8A117E-DBC9-4B11-AFFC-10588EE4839D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e07930ce4911f611d084d7578c97cdc8fb3f729","datavalue":{"value":{"entity-type":"item","numeric-id":2763694,"id":"Q2763694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q414899$AFB3D992-3AA8-43C9-AC36-4603113C20DE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"96019700171ab408d19f016759f09e5fa9366908","datavalue":{"value":"10.1016/J.JCSS.2011.05.003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q414899$30A11CBE-B2EB-4790-AD7F-C49938D4EB0A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"68ed007a86f6f0f6ba301afe4b8d842f36d917b3","datavalue":{"value":"The game-based approach offers a very elegant way for establishing properties of systems modeled by Kripke structures. The paper extends the game-based framework of \\(\\mu\\)-calculus model checking to the multi-valued setting. Structures in the multi-valued semantics are Kripke structures defined over a lattice. The meaning of a \\(\\mu\\)-calculus formula in a state \\(s\\) of the Kripke structure is an element of the lattice, called the value of the formula in \\(s\\). The task of the multi-valued model checking problem is then to compute the value of a given formula in a given state. This problem has many applications in verification, such as handling abstract or partial models, analyzing systems in the presence of inconsistent views, and performing temporal logic query checking.NEWLINENEWLINEThe paper defines a new game for the multi-valued model checking problem of the full \\(\\mu\\)-calculus, and demonstrates how to derive from it a direct model checking algorithm for its alternation-free fragment. The algorithm handles the multi-valued structure without any reduction. The paper discusses properties of the new game. It also shows that the usual resemblance between the automata-based and the game-based approach does not hold in the multi-valued setting and how it can be regained by changing the nature of the game.","type":"string"},"datatype":"string"},"type":"statement","id":"Q414899$8A4AC1FB-662E-44AC-A446-FC592D03D643","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28455a1e4bb6038f42a3a625d07f01f331a64fe3","datavalue":{"value":{"entity-type":"item","numeric-id":5491877,"id":"Q5491877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0709a2d9a5f6891b81cd83a33486c711c92f20f","datavalue":{"value":{"amount":"+0.9836519360542296","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":"Q414899$27BFD2FD-CA38-48DC-BE82-4E6E7E193A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b12f51fa7508470e8c4ac3504e447c6d1dcdb61","datavalue":{"value":{"entity-type":"item","numeric-id":5466469,"id":"Q5466469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"843ecff4296b9785282598e2aa828fff1b2b8130","datavalue":{"value":{"amount":"+0.8528420329093933","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":"Q414899$C86C5452-E344-457A-B3AC-6598DD307083","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca31711aaa221a2cb2e1d07abcdbe3134d735ffe","datavalue":{"value":{"entity-type":"item","numeric-id":5900571,"id":"Q5900571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"657613f9296e8a781a19d315264edfe5af9497e2","datavalue":{"value":{"amount":"+0.8270280957221985","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":"Q414899$7385E893-AA56-4E28-BDCE-18B56D8F07FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e72c57564b42540b67653ee9fe2c14a4d275e82c","datavalue":{"value":{"entity-type":"item","numeric-id":4450445,"id":"Q4450445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87ef3e1d5c52c719be6b1170c5ba403e1549378b","datavalue":{"value":{"amount":"+0.8090547919273376","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":"Q414899$A35DA6D0-9749-4747-ACC1-E38DEAF03C39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8cb451e9f4ce4a7f0b0192fa14e434bcec27dcb2","datavalue":{"value":{"entity-type":"item","numeric-id":3552519,"id":"Q3552519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4513ce33bc5b506cf58cd0301a2ad620db736ae8","datavalue":{"value":{"amount":"+0.8057546615600586","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":"Q414899$CA5AD179-6812-4CCF-96BA-965D5C4C8886","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Multi-valued model checking games","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Multi-valued_model_checking_games"}}}}}