{"entities":{"Q2351397":{"pageid":2362140,"ns":120,"title":"Item:Q2351397","lastrevid":72576528,"modified":"2026-04-14T05:51:48Z","type":"item","id":"Q2351397","labels":{"en":{"language":"en","value":"Finite reasons for safety. Parameterized verification by finite model finding"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6449233"}},"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":"Q2351397$8DAD4000-B1B5-4553-9A15-DCA105B15329","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a8c0c1ed68b681de4ddb3f2ff18cf9da9640b577","datavalue":{"value":{"text":"Finite reasons for safety","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2351397$DF30A758-0948-4F09-8D01-E7415897DDC1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"87df1e80d53dee61ecd8b867b53ab038cf1dff12","datavalue":{"value":"1314.68185","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351397$B1F91A62-0CBA-4E2B-8C61-75B544E5D27B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$00136731-6F8B-47B1-B357-9E32F3B9DC3F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c61f53f8f8d7719eaa1ef54a22f9b50ec39aa46f","datavalue":{"value":{"time":"+2015-06-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2351397$1A4A59BF-E8AE-457B-82A4-140E0D470134","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351397$6F89AFFA-95C5-4D93-9734-1D26A04DC0BD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f9f6f0031793db98f1926e7c8d42b5bbfe718ee9","datavalue":{"value":"6449233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351397$62B82C1F-42F3-47E8-B0F7-F27A90F77435","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d07fa6664c279b971fd3f8ef7147fe2b074581e6","datavalue":{"value":"finite model finding","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351397$100BB4CB-6E56-4ACB-BDC6-9CD3787BD79C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"669abbb88c892b9db5795fabf18f855789fc40f1","datavalue":{"value":"parameterized verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351397$8F166B24-F3E4-437B-88BD-7859E5FACC62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"995b00cc7d69ee07cf24da51a3a5485ed2bb2d30","datavalue":{"value":"mutual exclusion","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351397$49240660-3E4E-4FC4-A533-66BA360B8625","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b97f3ef525532e6c28402d0d37eb7ab168dc2572","datavalue":{"value":"monotonic abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351397$49DFAD5E-B3D0-4712-A46A-DA9A89CFA725","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d339f391744d71a42c1c3f5aca1b4f8a3d35b415","datavalue":{"value":"regular invariants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2351397$5CFFA150-85FC-4171-A413-CAC827AEA324","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fd2028c5945640f27cb6959a4899c9e5ecc937af","datavalue":{"value":{"entity-type":"item","numeric-id":18923,"id":"Q18923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$9F9BD195-E549-4F2E-91C3-CC5F467B321A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f72920035b67b72d36194fa1cacb9706003d48fb","datavalue":{"value":{"entity-type":"item","numeric-id":23847,"id":"Q23847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$EF349B7C-0C84-494C-B38F-E1C5438ED1BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"82659ddd3b24a7f3c51a78eb5f25cc1e5d64df69","datavalue":{"value":{"entity-type":"item","numeric-id":17116,"id":"Q17116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$7CCEE361-0E4D-4838-9E10-EB7DAD385516","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2207b0b201a95a431b254bcb1c01d869b9f41774","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$B712A3CD-5540-4835-81F8-B2C983AB6A96","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"95e9100254d03da2193ebcb0473e06193cec5626","datavalue":{"value":{"entity-type":"item","numeric-id":1662268,"id":"Q1662268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$FFD70C7C-1721-43B4-9686-9BA50D1EF040","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":"Q2351397$4B050698-B316-4A50-A8DC-0C3B624EFB13","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"43e52016f5424e77b819fdf9662be6b4cbe9a94d","datavalue":{"value":"https://doi.org/10.1007/s10817-013-9274-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q2351397$EDCC4DBA-2E99-4E31-B1D2-07BAF1A9BF1D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a9bb90722d9a62b482a32de91786b334bccbabda","datavalue":{"value":"W10211586","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351397$660BFC58-28BD-41B0-9D3C-4F249061B9BA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dca640f3efd730e5f875de06c5db75843c006cff","datavalue":{"value":{"entity-type":"item","numeric-id":1923094,"id":"Q1923094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$0CD0ECBB-04BC-4819-9104-B956DA8808D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1db59f76df444163b20fefb5198b53fe84a10a83","datavalue":{"value":{"entity-type":"item","numeric-id":3646165,"id":"Q3646165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$CA9288B3-22EB-40F3-A7AD-B0DCFCE068FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a14f991dbd8778adffefe5f5053765292d1e6033","datavalue":{"value":{"entity-type":"item","numeric-id":429586,"id":"Q429586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$0E239D76-E8EE-4B03-BCE1-8421A32B4607","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f0b555d657cb1f5a17dad4f6c65786062114626","datavalue":{"value":{"entity-type":"item","numeric-id":2487870,"id":"Q2487870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$F2B74DE5-3522-4649-8C50-BCBA1BA63038","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2fe32806edf287e44f6855c200795e18b751477f","datavalue":{"value":{"entity-type":"item","numeric-id":2751366,"id":"Q2751366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$286FB926-F511-48C4-8230-99BA3087B79D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88513da3b40e8d94cc45b6d0ad9dbb72de7a7e33","datavalue":{"value":{"entity-type":"item","numeric-id":1878907,"id":"Q1878907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$680CD45A-B49D-4CF1-A934-C356953275F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$3F931089-A163-49CA-93DD-C43C7D1CAA51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78c5fa7f8966f430b51e2a366e8bc01608e75588","datavalue":{"value":{"entity-type":"item","numeric-id":4474215,"id":"Q4474215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$26F5EE19-D9E0-4F0B-BFEB-4551292C44F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cdb831970cdc01d205b526f08958ccd77a1ab13","datavalue":{"value":{"entity-type":"item","numeric-id":5747748,"id":"Q5747748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$92A9B85A-3010-470D-9CE5-885CF7E421BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3c468c5df999a5df8b9ca61276e57be905929fe","datavalue":{"value":{"entity-type":"item","numeric-id":3541687,"id":"Q3541687"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$72D4144F-9619-4A0C-ABFB-5060E576168C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35464b2decff7913546b425f92c449bf65073e1a","datavalue":{"value":{"entity-type":"item","numeric-id":5146597,"id":"Q5146597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$74364268-22E2-42AC-B2C9-6CA23053F711","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22addb5f3a51b2f17fcb41951064c05876e03255","datavalue":{"value":{"entity-type":"item","numeric-id":2851061,"id":"Q2851061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$81E6EA30-05FE-4A39-95FC-DD3FDD029AFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cfe99189527a8421941693fee61786582f38d792","datavalue":{"value":{"entity-type":"item","numeric-id":3184717,"id":"Q3184717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$458BDDC1-D956-4EA0-95B1-0C452F7D181A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b989303c3f01780ec3752ac791fe5233d16a37b4","datavalue":{"value":{"entity-type":"item","numeric-id":1094888,"id":"Q1094888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$BA93535F-7825-4783-9DD7-473A6D4151D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afe18fdfb882c799d34a7482b763d96a45625e71","datavalue":{"value":{"entity-type":"item","numeric-id":3853827,"id":"Q3853827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$4AA99361-3CC4-4C5C-BD34-B00019F06D57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"730cc11830726606198273646645dafdf3dbf998","datavalue":{"value":{"entity-type":"item","numeric-id":4931295,"id":"Q4931295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$56E1D4EB-480D-4366-878A-1409C4D6A257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f401db670261330664f5823ed2c901ce74b45ab","datavalue":{"value":{"entity-type":"item","numeric-id":5111907,"id":"Q5111907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$527EEECD-892B-47A1-AE15-6420F565D9DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86863697a38444bb750622f38f93dfb010d37b48","datavalue":{"value":{"entity-type":"item","numeric-id":4953405,"id":"Q4953405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$10DD4BFC-4E63-42AB-B7F0-EAF3E6C5BF55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16005f89f06fee989030d39fdcc1703851f6718b","datavalue":{"value":{"entity-type":"item","numeric-id":2841218,"id":"Q2841218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$19D181BC-1EA2-4D93-8AC7-96BE28E83927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43f8b81729c278d2b25a84d10accbf70874b133d","datavalue":{"value":{"entity-type":"item","numeric-id":4263167,"id":"Q4263167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2351397$AF3A63DA-D09D-4956-92CC-88F63FC07CB1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8c053e66f00a30362df84d06233e0f9fa014783f","datavalue":{"value":"10.1007/S10817-013-9274-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2351397$C97CF1F7-7861-4AD8-8B8B-66773C113441","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6206dd76673762637ce922be8464826ad4594d38","datavalue":{"value":{"entity-type":"item","numeric-id":4931295,"id":"Q4931295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"044741a88bdc275504b5cb73d3a94825a4bac1db","datavalue":{"value":{"amount":"+0.8758392333984375","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":"Q2351397$D371725A-96D5-4C91-A391-35BB5A0D5052","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"91fa8a0c4336e646769ad9d9c388805218b1918e","datavalue":{"value":{"entity-type":"item","numeric-id":4472240,"id":"Q4472240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7005560dab6e36c82d94ff84f0f026cb20edb175","datavalue":{"value":{"amount":"+0.8014575839042664","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":"Q2351397$BB22B691-9DAD-4BFA-876F-6F8FBEC3B5AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3fb76d0b07e62cdcb89da7023e2e933f2be3933c","datavalue":{"value":{"entity-type":"item","numeric-id":5111907,"id":"Q5111907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"707fb163e69ed1ec4c1ec1a1864189f7b59997ae","datavalue":{"value":{"amount":"+0.7976697087287903","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":"Q2351397$C97EF89F-46C8-45EC-A990-80E96AECEEE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65cbaf1e979b491d7a6e5f7ade5d53365f7dd855","datavalue":{"value":{"entity-type":"item","numeric-id":1886449,"id":"Q1886449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d999c0826671b3698286bcd494eef5fe4546978","datavalue":{"value":{"amount":"+0.7886727452278137","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":"Q2351397$4D6E5B42-FC22-41FF-9CD7-AD5CCF89CEEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e88d80e9074cfb0b5ba6a572c8ecfc53b22b379","datavalue":{"value":{"entity-type":"item","numeric-id":4414374,"id":"Q4414374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93f55da0913547d2092f77443d82f24bc0c0279d","datavalue":{"value":{"amount":"+0.7850995063781738","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":"Q2351397$2528E380-00E3-45E5-B66B-E7AC16EB9D90","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Finite reasons for safety. Parameterized verification by finite model finding","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Finite_reasons_for_safety._Parameterized_verification_by_finite_model_finding"}}}}}