{"entities":{"Q4255977":{"pageid":6285578,"ns":120,"title":"Item:Q4255977","lastrevid":46837002,"modified":"2025-12-25T16:55:26Z","type":"item","id":"Q4255977","labels":{"en":{"language":"en","value":"Model checking lattices: using and reasoning about information orders for abstraction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1308926"}},"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":"Q4255977$7E8E3FA4-A0E7-4E35-848D-663508C02133","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ff084a754b3bb89f824909f29ef9670c92eef712","datavalue":{"value":{"text":"Model checking lattices: using and reasoning about information orders for abstraction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4255977$2D50A9BA-6BA7-4A68-A421-31246219ED04","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bb912d13c056a906953152347307b0de696072df","datavalue":{"value":"0930.03031","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$58534437-D57B-467E-8743-33E462A9F56F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d0e6a88f6f734251f9a8cb9684a762d9b44a2184","datavalue":{"value":{"entity-type":"item","numeric-id":4255976,"id":"Q4255976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4255977$AD9858BC-5627-4EB2-A85D-88711E5A1508","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8805eb347b0d2233a80238b7549669d8e629fe79","datavalue":{"value":{"entity-type":"item","numeric-id":526774,"id":"Q526774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4255977$BBB10592-B664-4DB1-8675-F54B67D33001","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8b5bfa12347d4716af416e8493dcfe0d9b94cba5","datavalue":{"value":{"time":"+2000-02-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4255977$3F5CB5FC-50D8-4C41-9FF5-B50C2C3091E1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$45E7C539-D812-4058-963A-B3BAA589609A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$92B486FC-99C5-4CF5-A61B-8A76E2AE5323","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$6CC80909-A1D2-44CD-8119-B952579E6222","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$39D36789-542D-4A53-A029-BFFAF222C621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bf715f882d7ad0c07303aa3e6e3ac3725da52515","datavalue":{"value":"03B50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$498166BE-FBF3-48FD-8212-ACC426FA7654","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"17dfb9705785520994ff40e9c7009b9dbef98ab2","datavalue":{"value":"1308926","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$57650186-9CF4-4DD6-8D2C-3521410EB6D2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4fe6a4db7f6d4f320025a2c13e14a4633c9dceaf","datavalue":{"value":"symbolic trajectory evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$4A494916-FD76-445F-888F-BF3E5411841F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"918868c8a8dc18dfc90be14b9937478d5d748fcd","datavalue":{"value":"quaternary logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$34DD305B-3306-42C1-908A-142AB8E1E05A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"733b3864b2e289419346b04e496da3a7a333fdbd","datavalue":{"value":"bilattices","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$5FE64D94-82E3-423E-B80B-E06E3EC2B8EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ab914e4b1ee636749aaff08903c675f2353b5ff","datavalue":{"value":"state explosion","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$99A71A99-AC06-4B22-B457-B767E0454004","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c20b4fa4782bc26ad106d3b73d2e44447725459e","datavalue":{"value":"automatic verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$982C7983-FD04-4BE8-924C-9940FC275544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$FCC69C4F-C70F-4E1D-9D91-AFE07B19EE10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6ef98f35ce99dd2d447b0b216c2c553732a3b0e","datavalue":{"value":"very large state spaces","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$5DF2DFFA-16F1-416E-B924-4EA536255356","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"379148470c56568e002eaf28d2db1b730e7a184a","datavalue":{"value":"information ordering","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$5B0C33AD-AEB2-4DDE-8BDE-8DE9A44AFBA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a71af8421218a4d8298f53de1a26b02e8634dc77","datavalue":{"value":"contradictory information","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$9B536475-7947-4412-A9C1-1C86B49AA790","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c98317212916950e0b1621fd14b923afc0ac0080","datavalue":{"value":"four-valued temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$7EBC43B0-739A-430A-B8AD-52E1B9FF77B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac52900f9c775a1c2e9b77521a060cf4681ca7f4","datavalue":{"value":"hardware verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4255977$4C92AC00-0551-4AA3-AA6A-CC6CCB1B676B","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":"Q4255977$6F6DBCEA-78E3-4E39-8AED-DC3CEF2BEAE8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"31b36b2782e96b5f5cddd6366f80dff354128ba6","datavalue":{"value":"https://doi.org/10.1093/jigpal/7.3.375","type":"string"},"datatype":"url"},"type":"statement","id":"Q4255977$F11F950A-326E-4D7C-9AE4-1DEDD40D6791","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f15dd453313729dd165f3274a72c9cef38b834ff","datavalue":{"value":"W1987507597","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$079A1A8D-66CA-4D56-AC84-C5B2D0F11C3B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c3d8213e9205e9649e1ad0d26fb0f8cfb10bd99a","datavalue":{"value":"10.1093/JIGPAL/7.3.375","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4255977$E04144A1-7645-4B3D-B797-EAB493A66C55","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2322a21df36f02b2b9c16a6174c764d5fc949009","datavalue":{"value":{"entity-type":"item","numeric-id":3061274,"id":"Q3061274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4255977$8095EA96-2603-4807-B060-035BF2F5F10D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49161caaa7eaf39f629db1a92ad320d38e825cea","datavalue":{"value":{"entity-type":"item","numeric-id":4472430,"id":"Q4472430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7c3e692fd4a6ca91e27b3192b9cd2aba5ec64db","datavalue":{"value":{"amount":"+0.7685356140136719","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":"Q4255977$F379397D-5D49-4A11-906A-A7F3A0860602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"760b067db9da312d12ef88c5b6830d46b4878de6","datavalue":{"value":{"entity-type":"item","numeric-id":4791849,"id":"Q4791849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c8b082640084db82d0ae17c91f982675184c842e","datavalue":{"value":{"amount":"+0.7474544048309326","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":"Q4255977$9D65AFF0-AA7A-4A7A-B3B4-3D21B6A88CA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1efbdcc87bdf4d278948a3598f0651896e7d1486","datavalue":{"value":{"entity-type":"item","numeric-id":1193587,"id":"Q1193587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bad580808316436bafe9186708214e3409444178","datavalue":{"value":{"amount":"+0.7456851005554199","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":"Q4255977$DD7A659C-608F-43D9-9E45-924CD001B7F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c502ff0941d8a169f2316d029902fab27cdd3337","datavalue":{"value":{"entity-type":"item","numeric-id":4818796,"id":"Q4818796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"318fa5eca14e268a691ac4626388df9b69b2e900","datavalue":{"value":{"amount":"+0.7430192828178406","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":"Q4255977$D4724EE8-AEDD-4C2E-AE55-C7858503F421","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4255977","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4255977"}}}}}