{"entities":{"Q883136":{"pageid":884984,"ns":120,"title":"Item:Q883136","lastrevid":65077608,"modified":"2026-04-12T00:10:13Z","type":"item","id":"Q883136","labels":{"en":{"language":"en","value":"From NuSMV to SPIN: Experiences with model checking flight guidance systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5159779"}},"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":"Q883136$FC54D80B-7825-497C-A9A7-8FEC6D51C8EE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aff523bc4a5ab7ed9130783c495668ccf849c67c","datavalue":{"value":{"text":"From NuSMV to SPIN: Experiences with model checking flight guidance systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q883136$EBE246BA-6DC2-4965-B4DF-7EBB0B1CB7F4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0d16d8a22b26d17fc78d76fa3493a2447a5bcce3","datavalue":{"value":"1111.68502","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883136$5857FCCD-8D9D-4E38-9459-DCEC57C32EDE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc79a50e71a794985930261c042a4c7a591b5c7d","datavalue":{"value":{"entity-type":"item","numeric-id":883135,"id":"Q883135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$2F4BE410-A90F-4190-A328-2F5BF7B7ECDF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$5F0CBDC5-8FE5-4FBA-81EC-719B98D86FF5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e35f0982f488bc16c2f1473de732103f14c19500","datavalue":{"value":{"time":"+2007-05-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q883136$87760E34-1A0C-43D9-9D47-39973E47C8FD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883136$DF6F54C9-93EF-4B2A-86BC-63673795658D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d19a5e2840f3750befad604cc7d1fd091dc3fe5","datavalue":{"value":"5159779","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883136$767267CB-066E-4E98-80EC-ADA8C4DB4975","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5541349f29c25ba6a0be12f614381c30b7057b17","datavalue":{"value":"Model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q883136$D9AA3421-9490-499B-9828-2CFE5E5DA557","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6441f2809d40f9de9f87212108670c34c553dfa9","datavalue":{"value":"Flight guidance systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q883136$1DDC0F2C-062F-4575-BC14-238828B63722","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"772c4ee50d131f1a35ff4b31da11ffcdcf02c815","datavalue":{"value":"SPIN","type":"string"},"datatype":"string"},"type":"statement","id":"Q883136$8E2EB23B-FAF5-48A9-A142-0AF2FA716EDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33e6e7fbc044e24a636f416a29bbfa6df53e6435","datavalue":{"value":"NuSMV","type":"string"},"datatype":"string"},"type":"statement","id":"Q883136$D3972AB5-A256-4DFE-A835-320FC2459B75","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"53a4a9b6c38d395d5b2eb80cedc3eefcbf3e9947","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$869DDEAC-0CD3-4DCF-AF5A-93B17E6D5E1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"efa7dfee3dd74aae04647605d0a9a987c7d566cf","datavalue":{"value":{"entity-type":"item","numeric-id":16316,"id":"Q16316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$036F99F3-1D13-4029-9B07-397C5D2580A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cc47147a404ecf949cf86c4e92d2dcc5a8bfafcc","datavalue":{"value":{"entity-type":"item","numeric-id":19680,"id":"Q19680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$85EDA7E3-124D-4790-BFD4-7A2C386681FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ccc062e2d311aa84366365333d09c3a4e32b41bc","datavalue":{"value":{"entity-type":"item","numeric-id":20934,"id":"Q20934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$F6F6F366-D5C3-448B-BB44-73EFDFFD5AEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"70849c7de8b1fba6771cc05a0e9adf71b0d9785e","datavalue":{"value":{"entity-type":"item","numeric-id":31835,"id":"Q31835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$F1ECC83C-08E1-4CC2-B97E-B75E52C09782","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":"Q883136$2263DFBC-E66F-4036-9154-5D32DCF9EEC2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d63d233b6cbdac2edffe79e5f232cd1a6b90497a","datavalue":{"value":"https://doi.org/10.1007/s10703-006-0027-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q883136$AAC3FFE0-88BD-4CD9-B027-8BE6315A25A8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6508203e2fa4570cb5e96c66fe66ebfe4843a33e","datavalue":{"value":"W2000117665","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883136$422D442D-6B27-445D-B186-85B5ABF946B2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"632009bd045b8ba41161b0002d2edcc70936c21e","datavalue":{"value":{"entity-type":"item","numeric-id":4738482,"id":"Q4738482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$99FBED21-1C88-41EA-BBD7-8B9BAA744ACB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a71df8b92ba7125a0c7197e8e9200d4d9ef576c","datavalue":{"value":{"entity-type":"item","numeric-id":1196296,"id":"Q1196296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$35BBB0CA-5338-40BF-B3CA-7837B6C8E3A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d189d5566bbdf8684108572f8e7b1cae5e8fb1c","datavalue":{"value":{"entity-type":"item","numeric-id":1595472,"id":"Q1595472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$F6B25C70-D15A-47B2-85BD-3249FDD2DE1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7d8c0e22cc6d5b8f5e5b95e505b643a065a9ef3","datavalue":{"value":{"entity-type":"item","numeric-id":1856163,"id":"Q1856163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$97021A48-DB37-424D-934F-B29E666CA69E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc18c9e2ac644564fdcbd6dbaf23e45f320cce72","datavalue":{"value":{"entity-type":"item","numeric-id":4818818,"id":"Q4818818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$B4A8A0C6-8EAC-4F7E-9B3D-DF508E1D8213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"841df77b5e5e2d994ab30d1be873a76e763763b2","datavalue":{"value":{"entity-type":"item","numeric-id":3345745,"id":"Q3345745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q883136$BBAE7E18-E946-43F3-8931-347E8605F1AF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cb39b736ed0e1b010ba3bd65a19b5a9b7162fcc3","datavalue":{"value":"10.1007/S10703-006-0027-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q883136$094FBD30-BEC8-4910-A8A7-B743FB22B69B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43fc7f092949fe15c38c6efb903e8bd4ff3607f7","datavalue":{"value":{"entity-type":"item","numeric-id":4738482,"id":"Q4738482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e163182b618590358b92b21bb147493009c7b11f","datavalue":{"value":{"amount":"+0.7822104096412659","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":"Q883136$5BE01DC0-EA70-492F-8AE9-6B2ED5CF444D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04d3f140e56d093502c355c663252673480b2e81","datavalue":{"value":{"entity-type":"item","numeric-id":2733893,"id":"Q2733893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"efee390e3e0da49a65d04ac8d602ad9c369b53fd","datavalue":{"value":{"amount":"+0.7571398615837097","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":"Q883136$12CE33AB-1270-4316-83A8-167D2166EAC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a361897a83fbcb8ac7951dffc524d62a5491ff4","datavalue":{"value":{"entity-type":"item","numeric-id":4494387,"id":"Q4494387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"435379a3812fc00c8188505161c8bca704de1da2","datavalue":{"value":{"amount":"+0.7571398019790649","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":"Q883136$1C6C6B8B-56D2-4F69-ABDD-D456100AD1F1","rank":"normal"},{"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":"31627cee1dd33abfa6b59f5670b3f90ae730d3fd","datavalue":{"value":{"amount":"+0.7561941146850586","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":"Q883136$423A1384-0FCF-4781-AFE9-2090577E78D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7406a6043450609f29a9adf09cf8e8c5eaa87040","datavalue":{"value":{"entity-type":"item","numeric-id":5452300,"id":"Q5452300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b15100b20c1f6098d6ab189ece54393f848135a9","datavalue":{"value":{"amount":"+0.7535090446472168","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":"Q883136$61CA45F4-FD65-4314-A02A-ECFC395F00C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"From NuSMV to SPIN: Experiences with model checking flight guidance systems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/From_NuSMV_to_SPIN:_Experiences_with_model_checking_flight_guidance_systems"}}}}}