{"entities":{"Q682350":{"pageid":684199,"ns":120,"title":"Item:Q682350","lastrevid":63774810,"modified":"2026-04-11T15:27:48Z","type":"item","id":"Q682350","labels":{"en":{"language":"en","value":"Formal verification of an executable LTL model checker with partial order reduction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6833661"}},"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":"Q682350$33694077-D159-4D3D-8707-431A5EED99B4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f0c7a6ece9ec440d3e4a3ef6d8f075f27105e540","datavalue":{"value":{"text":"Formal verification of an executable LTL model checker with partial order reduction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q682350$1E466E45-2A62-45F0-88DC-3B4CB14C3D1E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"50b7d7f37ec9e18da26a4e24a8a469733c3674cd","datavalue":{"value":"1426.68162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682350$A2A6A1FA-3E8F-430E-BE07-87E9935C24F8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9208c686420f2aa6176db085d3d2a8eb090b48fb","datavalue":{"value":{"entity-type":"item","numeric-id":682348,"id":"Q682348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$8B354D0E-BEF2-4768-9003-1ADA82D7BE62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8e4be225a6094490d6530fbb2f56929f5bbbcf0","datavalue":{"value":{"entity-type":"item","numeric-id":682349,"id":"Q682349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$E0C7910D-3B30-434A-9022-B2FA1881D086","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":"Q682350$215427EF-F411-40D5-8FCC-AE997F67781A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3340cc79e75714646430612898cfc312969e0dd0","datavalue":{"value":{"time":"+2018-02-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q682350$1C583CC4-2AD4-46F3-8CA0-123C5445CB84","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fff6bef0cdb03a461ae2950002c293cc22c448d2","datavalue":{"value":"https://www.research.manchester.ac.uk/portal/en/publications/formal-verification-of-an-executable-ltl-model-checker-with-partial-order-reduction(a99dc6b6-0529-4ae7-860e-fd64f74c9912).html","type":"string"},"datatype":"url"},"type":"statement","id":"Q682350$B1FFB0B8-A1A7-483F-B7C9-39A6D42F9D28","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682350$DE2346C6-0BE2-46DB-84BE-5F43B8EC95A7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8ae4c98587568dc3ef0d830065e4e95c898ebe23","datavalue":{"value":"6833661","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682350$08A6DF02-C839-43AA-9FFA-AA740847EDCE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q682350$ABFB7FFE-8851-49B2-BB71-F5DB77BD9E9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q682350$9E5E52ED-3ECD-4B89-B916-2E49D42AD0AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4be0568078bdb23907326b194531a896f4c2e986","datavalue":{"value":"partial order reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q682350$ADBEA578-8D90-43DC-AF1D-F447150E7CDB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$6A5E6A82-08E8-4781-BA0B-F1D370F41D89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e8d40c421847de2e0ab01b9932e18d4bfbfa229","datavalue":{"value":{"entity-type":"item","numeric-id":40949,"id":"Q40949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$898125A4-274D-4F29-B2B4-08C6ECE66691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ac603bd33045b83a388c11f327340dad56128212","datavalue":{"value":{"entity-type":"item","numeric-id":40289,"id":"Q40289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$7D2F2DC9-12BE-4B60-96CB-1478056C67A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"98af688e1c934064642a1507ce8ad17cf34ce751","datavalue":{"value":{"entity-type":"item","numeric-id":40284,"id":"Q40284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$967858FB-3E10-4780-B4A6-E4B8CBB8FD69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"92b02fe24d8af7a83050fa893b2981eb358a3139","datavalue":{"value":{"entity-type":"item","numeric-id":40283,"id":"Q40283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$7BBDD6B9-E028-4182-A538-693C760F7DB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$DE081BFF-60CB-406D-AF39-E36C7C28594D","rank":"normal"},{"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":"Q682350$A536CEE2-1D6D-4272-B83D-4B233F83E797","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"07c77124a102677321b49e780d83d2e468dd9d6a","datavalue":{"value":{"entity-type":"item","numeric-id":19657,"id":"Q19657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$52729C4C-7BAC-4010-B570-A757D420F5D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"13e3c1ae037a69a0e955591f025dfaca47973868","datavalue":{"value":{"entity-type":"item","numeric-id":40265,"id":"Q40265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$AC74494B-28ED-452F-BDC8-48E54E6868DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"00eff5f4477a877589eb9cf8614492385c42b973","datavalue":{"value":{"entity-type":"item","numeric-id":40251,"id":"Q40251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$2E138A62-DC57-4070-83BE-5E7AB3C1EFAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a702409075e50310c4740b6b68ff6f044d831b5d","datavalue":{"value":{"entity-type":"item","numeric-id":40324,"id":"Q40324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$89B03361-4DC4-4944-B8AF-A317A3E994C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0fac9fb5cfad6545c88cc8857964533dffc3ed17","datavalue":{"value":{"entity-type":"item","numeric-id":40544,"id":"Q40544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$01E2CBEB-2674-4EB5-9E89-D2C993843BA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$5781DAC0-0378-4FD6-91AB-34989AE0B210","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"877fe43feeb6e906af8a2cba157afebe0734c128","datavalue":{"value":{"entity-type":"item","numeric-id":40629,"id":"Q40629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$D3D6CCC7-CC00-47DF-A270-13EE0BCB37BE","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":"Q682350$74E02D83-2684-48F4-ABF0-4F55058C9299","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ec7c41cec2503b77deb59fd431c3afeb47a51c7b","datavalue":{"value":"W2671604182","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682350$06D17915-E428-4CBE-97EC-E6E68B577302","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"79e807f14dcd5f9ad4f6bbeb1f8ea3c4bbb7d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":4396958,"id":"Q4396958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$F52B7225-19F6-4475-BFA3-01A08769E28F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4d993f7be3ea77cad4a800be898a39b5ce70ed5","datavalue":{"value":{"entity-type":"item","numeric-id":2879246,"id":"Q2879246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$9C807529-5FC2-493A-9398-69DB82A5AF86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"76b9c6c60f3db2907a04f9c3b63c103f4fca17c6","datavalue":{"value":{"entity-type":"item","numeric-id":682350,"id":"Q682350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$CDF895E1-124E-45AA-9AC5-0C20E3FC6A82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"31067e58485990e94b288d36b9237062670ad8fb","datavalue":{"value":{"entity-type":"item","numeric-id":4356435,"id":"Q4356435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$6E75E5A2-B7B6-4093-B277-A0DA4C949B27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7f766bae7bb1dc745731294a8b2405f79150a41","datavalue":{"value":{"entity-type":"item","numeric-id":2914741,"id":"Q2914741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$B0FF35E6-BDB5-4295-A0D8-DFCCC00630C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5dffe5441220fd05c9ab29a095f510d384d606b","datavalue":{"value":{"entity-type":"item","numeric-id":2945637,"id":"Q2945637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$01B5768B-5EDA-4355-A523-8899440262B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2235cb100f2692698d1e78c89e440355cd4f7add","datavalue":{"value":{"entity-type":"item","numeric-id":2879261,"id":"Q2879261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$C802EC95-E5C5-4EEE-99E1-4E837BB47518","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a5a326924c9f9f3cf0f5061fb0ff950ccfad0d","datavalue":{"value":{"entity-type":"item","numeric-id":5747660,"id":"Q5747660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$625BD572-E55D-4CB1-BBB5-EA3174E94266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7db5eb581c5550fe9f1aaa6318cbc6f909c56173","datavalue":{"value":{"entity-type":"item","numeric-id":3771629,"id":"Q3771629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$23C0E84B-924F-4F5C-9166-459586255B9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$1003CBD1-6117-4172-BFD2-023DDBB15E2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"747cc4de9ba2a5f1b34ac1e3a64be5300b4f97a7","datavalue":{"value":{"entity-type":"item","numeric-id":960506,"id":"Q960506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$0EDD353D-EF01-4C6F-8883-D472C546D3CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"857799d8f0c80d23f1693fb90d554f48eb5bb5a0","datavalue":{"value":{"entity-type":"item","numeric-id":290250,"id":"Q290250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$5E141E79-4F3E-497A-9B57-54B1C2DBC6DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b78cda30b8bf7bbc1e02364c4dd5fa066a61862","datavalue":{"value":{"entity-type":"item","numeric-id":4279255,"id":"Q4279255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q682350$37988FED-26A2-4916-92B4-8778464770F9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e271ea2776471ccac3dd7c45e341f728a323030a","datavalue":{"value":"10.1007/S10817-017-9418-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q682350$00B1C8B9-CDC4-4133-B71F-6C7B1C5D50A1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a222bf16251a8af35aa3c32835e189c02324c310","datavalue":{"value":{"entity-type":"item","numeric-id":1961915,"id":"Q1961915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2519dc2c07a493f493cc8f49a3334f040e05887","datavalue":{"value":{"amount":"+0.795279860496521","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":"Q682350$2686467C-4A69-41B1-BF84-F835C692BCA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c3e85a19d8cfd74e289991cadbea56498301d45","datavalue":{"value":{"entity-type":"item","numeric-id":736463,"id":"Q736463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39e5cd12faf28ca1518979c58c6ba8533f33f2da","datavalue":{"value":{"amount":"+0.7603974342346191","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":"Q682350$F559A76F-41BF-4BCB-970C-55825934A5E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8e41e11b55706db3aa67de98ac1c80e47db2dd1","datavalue":{"value":{"entity-type":"item","numeric-id":453518,"id":"Q453518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7e10353f6719f42c54800900d950141d9a71761","datavalue":{"value":{"amount":"+0.7591137886047363","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":"Q682350$391456BC-CE88-4D36-90DF-924A269A2E37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"050b4a2623d15e751baed2a171c14980626a591a","datavalue":{"value":{"entity-type":"item","numeric-id":960506,"id":"Q960506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1898e69848230cd4bbe05a23805f8f0871eaf83e","datavalue":{"value":{"amount":"+0.7579602003097534","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":"Q682350$2988C928-8DDE-4DEF-A1AF-E6A22FCDADB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27852a71dcb57134c3358ab1f2ff1fb7ac83fa04","datavalue":{"value":{"entity-type":"item","numeric-id":3183543,"id":"Q3183543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45d572424499efecfd7e6f4a0b5d6ca641328ab1","datavalue":{"value":{"amount":"+0.7570520043373108","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":"Q682350$920C4B93-63AC-4D20-8368-F558E7D9969F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal verification of an executable LTL model checker with partial order reduction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_verification_of_an_executable_LTL_model_checker_with_partial_order_reduction"}}}}}