{"entities":{"Q3648712":{"pageid":5678618,"ns":120,"title":"Item:Q3648712","lastrevid":90441923,"modified":"2026-06-04T20:11:59Z","type":"item","id":"Q3648712","labels":{"en":{"language":"en","value":"Symbolic CTL model checking of asynchronous systems using constrained saturation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5640949"}},"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":"Q3648712$DF6187DE-487D-40A8-972C-CF2D28AEB28A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1de643a49d60c6a128ae75c8b89e37af0dda91c3","datavalue":{"value":{"text":"Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3648712$F78C20CC-EC87-44A2-847D-E1FC6AB85816","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c1e23d85f3c0dab9f75ca59953de6c2325a59a1","datavalue":{"value":"1262.68132","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648712$FCE4085B-C7B7-4087-A340-45FD5D31D887","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8eb9c6f81278d0fc618b7ffb8d33cd075b1ef269","datavalue":{"value":"10.1007/978-3-642-04761-9_27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648712$EA9B9C8F-0512-46C5-8DA8-B7D06E760C5C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"33de0e0506492d88a5ed255e5d12fc82a3d531d4","datavalue":{"value":{"entity-type":"item","numeric-id":277998,"id":"Q277998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$DE791A30-D649-4A46-96ED-BECF813287CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f4a9452230b48b25729b39bc47037fb4f65b446","datavalue":{"value":{"entity-type":"item","numeric-id":2158284,"id":"Q2158284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$DAFE8D62-B7C7-4A55-92A1-23537DE9CD0D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fb871d7a444106c04a08900e781eca233868e362","datavalue":{"value":{"entity-type":"item","numeric-id":3172900,"id":"Q3172900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$90893912-201E-4853-ACC9-5C4F28A1E370","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b8bdd78fc222a44e05f767ee071ed0c7d623c0a6","datavalue":{"value":{"time":"+2009-12-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3648712$C4D3708F-7FA5-45FE-A053-E1787C9B78CC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648712$51E6D9C7-073D-4AD0-A750-1006EF8C5122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648712$324583F4-1978-4B26-96F1-CFCD1D5A93BF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e8a8196820c3acf98963912a1d16ce04614026cd","datavalue":{"value":"5640949","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648712$890883B8-3927-46A8-BF48-9BE1015CA66F","rank":"normal"}],"P1463":[{"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":"Q3648712$6F48680C-6374-4C1C-AE79-40AB6DC8BDF0","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":"Q3648712$7A28D1A9-4C24-4F92-AC19-5FB9F366235D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7cd26be3f4f287ffdf33811eb4a89284652f6dcc","datavalue":{"value":"https://doi.org/10.1007/978-3-642-04761-9_27","type":"string"},"datatype":"url"},"type":"statement","id":"Q3648712$BDF9FC20-4924-43F9-B9A3-8DC429E97DFE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"07a9cdaac21833ef85b97742a5786dbcb25a9fc9","datavalue":{"value":"W1569724714","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3648712$5DD5B4A0-3355-44B2-9EF1-7C95D960EEDD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f0618ab971b1402c4c34251dffc850ea86689a4","datavalue":{"value":{"entity-type":"item","numeric-id":1856168,"id":"Q1856168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$0BC90D7D-86E9-47F7-8CE4-1159B455D8DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d0863918228d158fae088a6efc6f79f2c8e8057","datavalue":{"value":{"entity-type":"item","numeric-id":3724245,"id":"Q3724245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$C43BD586-9AD6-4A73-A510-156DEE953166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a61000b964a88108517cf3ef5eb51eb15c394a2","datavalue":{"value":{"entity-type":"item","numeric-id":2642670,"id":"Q2642670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$D2BBABCC-F357-44C1-AC70-79DC6BA0E410","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4ffa9af707a9034e194333cec43fea04e458a9c","datavalue":{"value":{"entity-type":"item","numeric-id":2769596,"id":"Q2769596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$BBC06ECE-3E92-4655-B6FB-790640A70A2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f47650ce464fe5007b4b38448155ea201ded8748","datavalue":{"value":{"entity-type":"item","numeric-id":4417940,"id":"Q4417940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$2AF1DC14-8FE0-4E7D-8024-A33000BC769F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bd2c5cd71f06f0d453a4c1620e42585bdbf9c72","datavalue":{"value":{"entity-type":"item","numeric-id":5900669,"id":"Q5900669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$A9D7CEC7-610D-428D-8CC3-20F0E298782D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c896b4044b299c66680bcf8adebfbdfb1fea310d","datavalue":{"value":{"entity-type":"item","numeric-id":5493224,"id":"Q5493224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$F3733E91-B024-4CCD-B812-9316CB3D65B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f541623726371fa1e6609e8c2eef0b9f81a4c6c","datavalue":{"value":{"entity-type":"item","numeric-id":4804909,"id":"Q4804909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$E8C6C139-3902-4969-958F-F4317E931B36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77396f690896742c51874a019bde10a47ce7fc02","datavalue":{"value":{"entity-type":"item","numeric-id":3599106,"id":"Q3599106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3648712$EDA184B8-1A6A-422C-BECC-56A2D111AF76","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4fd8cb04b907fbacebed7e6781f04ca62833ed30","datavalue":{"value":{"entity-type":"item","numeric-id":5900669,"id":"Q5900669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc237683fead24f0b097fd4aa0fb548ca3a77eeb","datavalue":{"value":{"amount":"+0.8309735655784607","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":"Q3648712$711FB22E-36FA-4E82-A409-D60C917E18FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f07a362b1de0c6e4b50f4544d982bf6bbad87100","datavalue":{"value":{"entity-type":"item","numeric-id":5493224,"id":"Q5493224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"699288d71ac16bbeec54fc51c5ab38cac5f3fa70","datavalue":{"value":{"amount":"+0.8169066309928894","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":"Q3648712$03CB1DF0-1D95-45FB-8275-25335F1AABD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0cef618344d3a9613d63552d649db4feadbfd239","datavalue":{"value":{"entity-type":"item","numeric-id":2769596,"id":"Q2769596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64028c46392e62367615c8df7ba8b00dc0bce45b","datavalue":{"value":{"amount":"+0.8152478337287903","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":"Q3648712$DB83BCA7-950A-4C94-8495-8C2503980534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"974e0efd42fb163a438b8cd86c8ca828ce24edca","datavalue":{"value":{"entity-type":"item","numeric-id":2820781,"id":"Q2820781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bbfe5f8f0907dc4d00413090520b35cb36a42ff3","datavalue":{"value":{"amount":"+0.788612961769104","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":"Q3648712$CD7107A0-2109-4AFB-B7FA-EB6A3D94A8AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71b0093b2d20b1a12f28e95a14d7825e6b930755","datavalue":{"value":{"entity-type":"item","numeric-id":4417940,"id":"Q4417940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5623a4fc3d5a52870f97acf979fd48115e056aab","datavalue":{"value":{"amount":"+0.7740494608879089","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":"Q3648712$2F71278B-6B9D-4D1B-860D-2A58A0F3FEA2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Symbolic CTL model checking of asynchronous systems using constrained saturation","badges":[]}}}}}