{"entities":{"Q5194964":{"pageid":7224536,"ns":120,"title":"Item:Q5194964","lastrevid":53533058,"modified":"2026-01-25T04:49:23Z","type":"item","id":"Q5194964","labels":{"en":{"language":"en","value":"Saturation-based incremental LTL model checking with inductive proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7105983"}},"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":"Q5194964$0542AC55-BFD1-4673-9374-FFC8584893C6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"748ccd86fa4c499fbf998da5561586fea74f9a29","datavalue":{"value":{"text":"Saturation-Based Incremental LTL Model Checking with Inductive Proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5194964$20CC0E32-4911-4170-8B08-FAA54A5E47F7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"276c499af8373c34510501b2a4ad908dccce988a","datavalue":{"value":"1420.68135","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5194964$1CF27B6E-3088-4BF4-B50A-075FBAD02A90","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5ad1bf566866575a7b4ea698806ed5540ece6846","datavalue":{"value":"10.1007/978-3-662-46681-0_58","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5194964$8616B359-601A-446E-979F-25E368467C81","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7e2eb36f5a43e442ad030de533939226ef3ebc66","datavalue":{"value":{"entity-type":"item","numeric-id":510889,"id":"Q510889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5194964$542FD71B-057D-4553-9F4D-8B3EB2C934D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8a72efe6db5357348e5ca0556391565efeda0088","datavalue":{"value":{"entity-type":"item","numeric-id":510891,"id":"Q510891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5194964$7540D284-6926-4442-BCED-514BE2CF9740","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"84ea6ceef3ce1a0bfb8053b2ffda2d5c16a41c9e","datavalue":{"value":{"entity-type":"item","numeric-id":510890,"id":"Q510890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5194964$81DDE18F-4B9C-413E-8C93-A237FFEE99F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0592968ca544264561e740df02e52eaa7ac3f830","datavalue":{"value":{"entity-type":"item","numeric-id":510892,"id":"Q510892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5194964$11E0B775-3366-4D62-BBEA-E2B5B151A839","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5194964$124078E6-AFB2-4D52-90F5-1C8ACBB7454F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"860c75d427a5be90563ac8b1b9f2dee75426aaaa","datavalue":{"value":{"time":"+2019-09-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5194964$5E088550-4834-420C-8D0B-B61CAE40C6CD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c31b754f74dc80800503b4bbe2b718a56816f717","datavalue":{"value":"http://real.mtak.hu/24597/1/TACAS2015_MolnarEtAl.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5194964$79CE27B9-60DE-4185-84BA-B35BE2C2003D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5194964$C55C0E52-EC01-450C-A429-61C1F87C5D6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5194964$2AE594CD-92E4-4E82-B667-8F411780A72A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5194964$DB117894-0245-4890-BE43-ACFBD92A061E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"123f601d0aaf21457bb74cff09e65fbdeb5f6fdc","datavalue":{"value":"7105983","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5194964$E521CC2A-81FE-4C94-9ACF-985036646ABF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e37aa0f4f08e208e1a86c646ff1c22e2ad4c4fa3","datavalue":{"value":"state space","type":"string"},"datatype":"string"},"type":"statement","id":"Q5194964$2E648CDE-59CE-48A6-9D88-F9301DCCEDC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5194964$21A318CA-1508-4ECE-84CD-8ED4ED800C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f1cf12c900aeb5813ce8f84db8812e6bb27ae87","datavalue":{"value":"linear temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5194964$69051912-7AAF-48B9-BF03-A1B5880479E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5eb7f00ee7fdadd911515b91bdfee9f839c293b4","datavalue":{"value":"concurrent system","type":"string"},"datatype":"string"},"type":"statement","id":"Q5194964$0AF6978A-C1E8-493B-8E58-B86F7125B91F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e7570fe1ab591c11640c69b073c4dbc2a3bc783","datavalue":{"value":"inductive proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q5194964$E9CD208B-4C15-4E74-AB3D-862862AA00C1","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":"Q5194964$9AE483F1-4A76-480E-8388-AD31E3DB4D70","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"936ecbfa77c650c382fc10ff43e9cef846f4f3a6","datavalue":{"value":"W1884765109","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5194964$1AFC9407-3DE8-4842-BBC6-961E4E04D4DF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d597a7dfd64e1269010e4d7e699cddb575cb1cc","datavalue":{"value":{"entity-type":"item","numeric-id":510894,"id":"Q510894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b0bf2bbb19a08d0797bed3d57d6904fd67ab4ae","datavalue":{"value":{"amount":"+0.923337459564209","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":"Q5194964$E33D6195-E53F-409B-9F49-7340CB6408BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2bb4627b13bef6d101489da2918850245c5e1b3","datavalue":{"value":{"entity-type":"item","numeric-id":3075471,"id":"Q3075471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b56a292404392dc22e7ada93efae83b5a658743b","datavalue":{"value":{"amount":"+0.7889194488525391","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":"Q5194964$F8EFC4EC-A2AA-4152-BF37-DE82A84F9CB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28f31bc5ee363ae455432d9f97fb1e41ae881ace","datavalue":{"value":{"entity-type":"item","numeric-id":5716576,"id":"Q5716576"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"af1d0ef00ad2ed3f19cf9d1715df2d47feb1ef0f","datavalue":{"value":{"amount":"+0.7694693803787231","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":"Q5194964$B5DA6179-B212-4A73-8A38-52593E72B27D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"070900cb1ccf70941d6282e43613f19432877cff","datavalue":{"value":{"entity-type":"item","numeric-id":3648712,"id":"Q3648712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce5d74c63db6825e41fe28b07c9288aafded9a63","datavalue":{"value":{"amount":"+0.7672612071037292","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":"Q5194964$CFFD6A0A-9443-44BF-9D8E-64C51A3EBCC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d55558c882eb537dea8b4ed637072d46a41d3d4c","datavalue":{"value":{"entity-type":"item","numeric-id":1707341,"id":"Q1707341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"002be75d71c5c00868b55cba2cc626ddc1dcb6fe","datavalue":{"value":{"amount":"+0.7666756510734558","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":"Q5194964$A84F1573-F0D9-4531-AB89-73AB3DED7966","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5194964","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5194964"}}}}}