{"entities":{"Q1193587":{"pageid":1204336,"ns":120,"title":"Item:Q1193587","lastrevid":42936211,"modified":"2025-07-16T04:48:09Z","type":"item","id":"Q1193587","labels":{"en":{"language":"en","value":"Symbolic model checking: \\(10^{20}\\) states and beyond"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 64869"}},"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":"Q1193587$C95017D5-0390-4534-AB62-044135A36317","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0024040d03709d1623971dd67c3255233aac07c7","datavalue":{"value":{"text":"Symbolic model checking: \\(10^{20}\\) states and beyond","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1193587$FC56AA34-0012-49D4-A8CE-98C6E4371DB1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"be4ef2c5b9e55fa8496e1d22eccf3c854caf7507","datavalue":{"value":"0753.68066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193587$EDAC55FF-0D5D-49B0-8BF3-41BE09779CD9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"89c32d507caded04970455da8e613704b642ef1c","datavalue":{"value":"10.1016/0890-5401(92)90017-A","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193587$C724B598-0338-4D01-8B80-2C93A98AAF2D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4e4e5ed72bee66087d415d4f69d49eefd101a453","datavalue":{"value":{"entity-type":"item","numeric-id":526749,"id":"Q526749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$3DFA2AA7-CA3E-48CA-8BD7-55817858A243","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57a84b3343ed70002617a9eb1439c18c15bac9ff","datavalue":{"value":{"entity-type":"item","numeric-id":934708,"id":"Q934708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$C56D43A1-C553-4B5C-9742-7E491E4611EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f0cc91cbdf8475d16a2827430a08885da3b0126b","datavalue":{"value":{"entity-type":"item","numeric-id":1193586,"id":"Q1193586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$AEA23958-CBAF-4619-BFE4-2231A106A457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"222205726dff0ef2b08bded726a14fc8cc9e5a10","datavalue":{"value":{"entity-type":"item","numeric-id":1076508,"id":"Q1076508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$EBFEC496-487C-4D0F-B6BF-5228BABFF093","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2dd061ef340feff0cbd009fd7ff490684b9da51c","datavalue":{"value":{"entity-type":"item","numeric-id":685109,"id":"Q685109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$129D760F-6D49-456C-96DE-2AD67AE7D917","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$B7BA7A50-7C89-463A-82FE-032627C1BAC5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5fd62271fe98c7ff9916cafed51cf35315eeeb31","datavalue":{"value":{"time":"+1992-09-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1193587$475A0B08-776C-41FC-9839-FB42CDF4503F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193587$B686054B-999F-484E-A222-45B6D5C375D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193587$1A9B5174-F754-44EC-8D3A-54315D912D1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193587$865D33BA-A609-44BD-8DC5-39DDFBC7D909","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9b33a79b5c63da97dc6cf193a738bd65c07acf39","datavalue":{"value":"64869","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1193587$33535197-0FCC-4640-9A4F-3262738AE0AB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ceda7008fe09fdf28806f1d5cdbb9e84182a0456","datavalue":{"value":"propositional linear temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$00E9228D-A275-4C1E-97F8-4085B51B4273","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75e78cd0204d4d31855e84e0e74f34cbe7774a40","datavalue":{"value":"computation tree logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$DF4356ED-0A06-44AB-8CC1-F3887BDFAA68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9ca8c7c8cead4c540d9788b20234085cc9b86447","datavalue":{"value":"symbolic representation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$221CFC41-CC5C-4981-87FC-19602F486D37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a2003496f989f52f10d8eb5f5940609debfc871","datavalue":{"value":"finite-state systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$EDB3EB2C-2593-4799-B537-5A93AF86ED5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7aa3fdbdf3b7584bcd007098b5e184978502a1cf","datavalue":{"value":"mu-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$77553C03-C7F0-4765-A70E-36DEB5F5D150","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bda86de3ee4e7c9902a8d526041721056eee9cf4","datavalue":{"value":"binary decision diagrams","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$618F4A48-4FA2-4FC5-AC2A-F4FD4B3F104C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d3542963eb421bb6af1e8ecde3c4376be009ba28","datavalue":{"value":"model checking algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$73223958-B4DF-476A-B701-CC0303B319FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ace8bf4699cb64394d0b2677300163ec8dcbc25","datavalue":{"value":"observational equivalence","type":"string"},"datatype":"string"},"type":"statement","id":"Q1193587$BB3D1242-B30B-496D-9743-3AC77B13DA26","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":"Q1193587$9C8E0BED-A3AB-41FF-BD90-A3212553AF9D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd1e5527beee43e76ace8195dd1167b63319c8cb","datavalue":{"value":{"entity-type":"item","numeric-id":3743249,"id":"Q3743249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$E43FD15C-CFA6-4BB4-9087-C4EA285FA751","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":"Q1193587$B85925D0-4320-45E8-9581-776B142D27B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e9d760b56e81829535236b574ab4988cdae3b4b","datavalue":{"value":{"entity-type":"item","numeric-id":3417010,"id":"Q3417010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$DE2605C4-5794-43BC-89CC-9371CCECA975","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf4fab5a4519bb0e4a7392865538dc50ad77fca2","datavalue":{"value":{"entity-type":"item","numeric-id":1193587,"id":"Q1193587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$BD8F4382-F224-4463-B23F-CDDF69F63ABC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d442c5d346825598cba0b99212b15bd39377066b","datavalue":{"value":{"entity-type":"item","numeric-id":685507,"id":"Q685507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$A9F3BEBB-BA59-419E-97D1-1FE043EEC227","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"731fff832e7711198e063399154f72f88c50c123","datavalue":{"value":{"entity-type":"item","numeric-id":3719811,"id":"Q3719811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$E4A6734D-0671-45D1-9E9E-0681015C5DBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a28e9cd35b47487d1554d6020ce3b8a9345efb1b","datavalue":{"value":{"entity-type":"item","numeric-id":4012209,"id":"Q4012209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$5974194E-41A6-4D71-B7C4-E095BF701991","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de1505d9b33c312794d5990cceccb798d2ac92bb","datavalue":{"value":{"entity-type":"item","numeric-id":4037382,"id":"Q4037382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$48559802-34B9-4A84-8E21-527343C2CEC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc95d446f80c52ed7453599d680e586168dabac7","datavalue":{"value":{"entity-type":"item","numeric-id":1327383,"id":"Q1327383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$DFF86C3A-150F-4578-A42B-4341C83F5ED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f5a45904f81b6a39ede475e2e86ab18eb54c04e","datavalue":{"value":{"entity-type":"item","numeric-id":801893,"id":"Q801893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$9AB9D14B-4CFB-40B7-873A-6E4C0AFE0793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c587e455f7abc58f3651f31b70f1918a721eb83","datavalue":{"value":{"entity-type":"item","numeric-id":4000225,"id":"Q4000225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$16CA6C5F-3725-44D2-AB05-7AF478C574A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a358a7e0cfe385397b6ee7256bfda7621794063","datavalue":{"value":{"entity-type":"item","numeric-id":3948585,"id":"Q3948585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$667E4270-AA4B-4EB2-99A2-5EA5361D6CBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60da585cac100a31c125360c9cbd2d207cbfe7df","datavalue":{"value":{"entity-type":"item","numeric-id":1148667,"id":"Q1148667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$ABAD303A-38C0-43C7-841B-F5ABB1788AA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f190ae2fde923a1f547028868c0453492060bbe","datavalue":{"value":{"entity-type":"item","numeric-id":1050111,"id":"Q1050111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$245FE4F3-29E7-411C-B6BA-863BE2880DFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa4614c3d7786f0db16d6ca3adbca9b075e1b1ff","datavalue":{"value":{"entity-type":"item","numeric-id":1177939,"id":"Q1177939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1193587$4787482D-4C4F-42FE-9CC4-8EB65121C788","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8f2b1d3bd200409369e68178cc9809d59dead18","datavalue":{"value":{"entity-type":"item","numeric-id":5448763,"id":"Q5448763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6665f9e3dd194e53749d0927cd972b934235df97","datavalue":{"value":{"amount":"+0.90472305","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1193587$65E231A4-9393-4741-ADB7-26663B2E0685","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94433ddcc3b1e1a51adee54d8cfb7b1456b7677d","datavalue":{"value":{"entity-type":"item","numeric-id":5432339,"id":"Q5432339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70e7d11500312193cb57984aca2faa3605a914c5","datavalue":{"value":{"amount":"+0.90166724","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1193587$D2E72172-AE35-4719-B3BC-E9B6391AEAD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ac3ed4b9dcd42e3112c1c51d9cea4b5d248e1c3","datavalue":{"value":{"entity-type":"item","numeric-id":3176389,"id":"Q3176389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"914448e65713b1966d3748b5b7e82c2743a29423","datavalue":{"value":{"amount":"+0.89380443","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1193587$7F30DAC6-FBA2-445C-BEF5-6E72901AB685","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1195558c560301d44336ee3c7e698d5b21c56cf","datavalue":{"value":{"entity-type":"item","numeric-id":2753716,"id":"Q2753716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b093519f20199bd4ec5dc8a85b2a2fd495de51f4","datavalue":{"value":{"amount":"+0.8915498","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1193587$049BC7BD-4AE1-45FD-ADE7-8CD2A81A81D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"662f051937086bb2907463bf6ee78e7b61ae81e9","datavalue":{"value":{"entity-type":"item","numeric-id":4493882,"id":"Q4493882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f58e9b835381f516365decc1df294c012a8dd8c1","datavalue":{"value":{"amount":"+0.89074504","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1193587$460A061D-F6BF-41F4-87A6-56DB5AC504CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"664ee6ce245c2bec86eb5428568691fb1e0409cc","datavalue":{"value":{"entity-type":"item","numeric-id":5505552,"id":"Q5505552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ca554d90abebba669b13ed566346a366b0339ed","datavalue":{"value":{"amount":"+0.88303405","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1193587$EBEC7620-36F9-4891-9BD0-6DA96DD33647","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c69faafc396cc37ce56ba7f317e1689803b3e471","datavalue":{"value":{"entity-type":"item","numeric-id":5941102,"id":"Q5941102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23d14ccf7d0c8796746ff421a8f2f4448a68b0e1","datavalue":{"value":{"amount":"+0.87767094","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1193587$B3987581-8A7A-4B45-AF4B-9F7B664D7F17","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1193587","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1193587"}}}}}