{"entities":{"Q6938564":{"pageid":21135006,"ns":120,"title":"Item:Q6938564","lastrevid":84106631,"modified":"2026-05-10T05:45:31Z","type":"item","id":"Q6938564","labels":{"en":{"language":"en","value":"Predicate abstraction for hyperliveness verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8084614"}},"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":"Q6938564$2D58E7B3-EA23-47CD-B127-DB8F196C67B5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c6d949228d1a90fd73f91f29691fd67469cf7fd7","datavalue":{"value":{"text":"Predicate abstraction for hyperliveness verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6938564$2F7FCF1D-9901-40E5-8034-487D1D2F8A37","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"293a15f856937cd0b967317a4b56040589a5d197","datavalue":{"value":"1571.68116","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6938564$DF2581CF-DF1D-4A47-B96C-ED933230EBAE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d08db8f2fcb2e2473c15c40a292483a21c1d1145","datavalue":{"value":"10.1007/S10703-025-00482-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6938564$78A3A35F-33F7-4F43-9F0B-ADED2B7085D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"eee58e07e7f9770d69c36e7da6f9baba391fe757","datavalue":{"value":{"entity-type":"item","numeric-id":5875387,"id":"Q5875387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$A119978D-E994-4748-B036-A9C2AE5CA9AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dda9ef52c721036bc2c5ca8408bcb7b43075ffbb","datavalue":{"value":{"entity-type":"item","numeric-id":515653,"id":"Q515653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$B1BDA3E5-6C1F-4C42-AC88-9019D923CDB2","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":"Q6938564$9ACDADA9-520B-4106-8E47-0D5DC92262E8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5524f65dba04a4e42636027eef156c68c8569d17","datavalue":{"value":{"time":"+2025-08-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6938564$C6E62BD6-E9AF-4F6C-B02A-DEB1AFAD32DD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6938564$C0016F60-97AC-4DDF-9F94-A412DB079E9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6938564$7F38B9E1-8456-4A5B-A0A3-080BF311353E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9ae239db43f925f180785d8e99a8fa2b121bf5f8","datavalue":{"value":"8084614","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6938564$BC430609-6B58-4018-8DC6-F77729B8A4AE","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$B09FB9F3-B556-4FEB-A4C4-837135231C00","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e4b9d662df2643fc95ad035c9e056cc88201723","datavalue":{"value":"hyperproperties","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$09502EAF-C519-4748-A707-E86C06B4707D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af88aa3d491903c7f03d61812402065edf91d808","datavalue":{"value":"hyperLTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$FB615B9F-E7D9-4F46-8F49-5962E938F11A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33091d86905202af08d9012d6e5fba9f5ed72f62","datavalue":{"value":"infinite-state systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$A2E78D9B-2E34-4EDE-BC87-B231BFF27AF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$ED06DE6A-DCAD-4846-89B4-9EA3BFD8D6E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9fb50508d9ae1a4b5b2525656ffbf4223c07463","datavalue":{"value":"predicate abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$2965A71F-F41B-4B71-ACD3-874EC056A97F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"23d77e85cae6ce25f59d36d8b3307a2b5410ad75","datavalue":{"value":"hyperliveness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$76A62753-9670-47AA-908A-87C72CBA4B8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$E2B98D5E-B998-4301-9224-169AA99F6695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"940b0739632e21f0e6fb7821d4c99956c66a10e3","datavalue":{"value":"program reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6938564$50E298AB-1367-4710-BEE2-1F6D2B646941","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":"Q6938564$675865E3-0D16-4D98-82A9-C7E481299BAA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5d5978f4bdf14ef5fd8b71ce390dbec5034a1e6","datavalue":{"value":{"entity-type":"item","numeric-id":805251,"id":"Q805251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$8ED77079-CE11-4497-A1BD-6B57C65FDFF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bedf9942225faf979656370f4108eb382224db37","datavalue":{"value":{"entity-type":"item","numeric-id":1064056,"id":"Q1064056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$0A4EF010-5BB4-43A4-8B70-52B35AD44989","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e8484a4d0dd98795f30cf5ed95fd68d76cc3ac7","datavalue":{"value":{"entity-type":"item","numeric-id":832242,"id":"Q832242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$0C23087A-A01F-463F-92B6-575B920C4887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3b3a3f4b3f44b312014bf38e16d46d1bd8aea8c","datavalue":{"value":{"entity-type":"item","numeric-id":5716568,"id":"Q5716568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$64E18431-2A3C-431C-B12D-66160E52C06A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"890db7446e2310e3c1bd99c02cf47b64ec54941b","datavalue":{"value":{"entity-type":"item","numeric-id":3455833,"id":"Q3455833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$04747C90-D572-466B-AE94-214AE0708C04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a486f6f61fd4d307e4fee9b67b4596eca0595e4","datavalue":{"value":{"entity-type":"item","numeric-id":3103613,"id":"Q3103613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$2E520307-0D24-40AA-BE17-E59CA77026AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba5ad8860e2dfafdd492a4ade42b23f462631c32","datavalue":{"value":{"entity-type":"item","numeric-id":5261508,"id":"Q5261508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$333E6488-3231-4425-8901-AF64EAF5B423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2d2c73a35c5eb7c6d2c5e9a70ffc488c6ef7353","datavalue":{"value":{"entity-type":"item","numeric-id":6967327,"id":"Q6967327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$38B9197A-E16D-4D20-A877-10D329EC3674","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f6571451eb34c2ec047797471dff827c46fd6e0","datavalue":{"value":{"entity-type":"item","numeric-id":832224,"id":"Q832224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$6B27BA86-1EB6-40D0-A9A9-84029E0638D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"902d58911cf57d61e4e30d431d92c375a51f10b6","datavalue":{"value":{"entity-type":"item","numeric-id":3452246,"id":"Q3452246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$E57A59A4-B4CD-45B5-9A09-2FAD820D5285","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0abc9bd837ab8b0bcca67e88ca9afbb772dbf1a2","datavalue":{"value":{"entity-type":"item","numeric-id":4800258,"id":"Q4800258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$8A538705-2BD3-4E14-B4E3-15AF68E91A6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"223cecbfff4cdc78f1be55791487409edaf065d5","datavalue":{"value":{"entity-type":"item","numeric-id":6649493,"id":"Q6649493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$C586880C-3CB6-4174-AEBC-60C6E323C358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cd41312b2e7671b43baf61c3a5d18d0b14b9edd","datavalue":{"value":{"entity-type":"item","numeric-id":6176108,"id":"Q6176108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$1EC5D9C2-1734-4CA3-802B-B51896E9D23E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1af4c8628c39415db8532d7ed1923a812de2f281","datavalue":{"value":{"entity-type":"item","numeric-id":6487322,"id":"Q6487322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$9EC98666-12D9-40AE-B73C-DEB8F6CD1CDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3215fe9ac9098da832062641028e1eb7e94dc9d","datavalue":{"value":{"entity-type":"item","numeric-id":6535349,"id":"Q6535349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$1745B746-599E-4DF7-B961-E5197B345590","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a61fc61652a4e833852385a8191ca3ffee37d00","datavalue":{"value":{"entity-type":"item","numeric-id":6135762,"id":"Q6135762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$D7483A16-D31B-4EE6-BFA0-46E23CC3C618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72c34d0fd3dc296bb7050a1892906d2d31cff1b7","datavalue":{"value":{"entity-type":"item","numeric-id":6535541,"id":"Q6535541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$88A900EA-4C68-4496-84EB-B27138153DF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"767027371f47351446d56e4b3b6a09eabc8be672","datavalue":{"value":{"entity-type":"item","numeric-id":5408418,"id":"Q5408418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$0A0EAEFB-E12C-4A7C-88E6-76F71B859DED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fca2fcee1fd6919a0db354b6be3a6754db0afc06","datavalue":{"value":{"entity-type":"item","numeric-id":2949438,"id":"Q2949438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$D8C56539-4EA6-439A-8E26-A24683C57BA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a19620c250c7c146c091f49035e11565f2887a27","datavalue":{"value":{"entity-type":"item","numeric-id":6651942,"id":"Q6651942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$01A80C94-A642-4D39-83FC-8334D6B5F922","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"839806caf5a65a073d1c277b709b43ecd8f87f4e","datavalue":{"value":{"entity-type":"item","numeric-id":6587135,"id":"Q6587135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$CCBF9E3E-FB60-41D6-84A1-EDAE6A63FAC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af7a415575615b2e42302790d11e106d39b1608f","datavalue":{"value":{"entity-type":"item","numeric-id":6154578,"id":"Q6154578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$3EE4DEDE-AD4A-4A79-960A-22C779C76352","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a84872841e456c541578d17e5a87958b215028f","datavalue":{"value":{"entity-type":"item","numeric-id":2151231,"id":"Q2151231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$F47A0798-CA72-4AFB-89D0-CC12AF13D281","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f94e8f311e50dd2a6565a5d26beb73e39be23ae8","datavalue":{"value":{"entity-type":"item","numeric-id":2988635,"id":"Q2988635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$5879DF12-EC85-42A5-A48A-4E07D8FE49CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"866f925d014efb82855c7942c0ce771392c27438","datavalue":{"value":{"entity-type":"item","numeric-id":3525630,"id":"Q3525630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$AD34E4E5-F2DA-4E1A-B61B-1865C1FA4D98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2061ba50cd825c7383ec471b4c6285950511fa03","datavalue":{"value":{"entity-type":"item","numeric-id":6176567,"id":"Q6176567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$785E004E-0697-4D87-8279-F3AAC73C7709","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"681d1a060becef7034c76396e1df8cd15b1e43c9","datavalue":{"value":{"entity-type":"item","numeric-id":6194574,"id":"Q6194574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$2F447D16-0217-4373-8A58-8446157BC58A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8be379e4dc29012717f03e4095ea9a22614ac5f","datavalue":{"value":{"entity-type":"item","numeric-id":1702908,"id":"Q1702908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$CC0E249E-9800-4873-929E-83AB9E6E7D30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acde43aadb68c83ae4d51574dcef8cc0958b2d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3392921,"id":"Q3392921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$9BA888E1-1018-4548-B8F2-09F3B81B4302","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91c21e537ab0c07b0d3849b9a7e5a291ced75540","datavalue":{"value":{"entity-type":"item","numeric-id":5178898,"id":"Q5178898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$7D783900-DC15-4542-A005-1D04D3945D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8edbe854d3e5f5f690729c125c1627884cc1d20b","datavalue":{"value":{"entity-type":"item","numeric-id":2044193,"id":"Q2044193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$25926D79-68A2-4CA6-B3E5-CEB887E0D00F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"32cf75770c4378a7060a1800d601a78571430882","datavalue":{"value":{"entity-type":"item","numeric-id":3176373,"id":"Q3176373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$CA809624-6E3A-4729-B972-47B06E0D15DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a18b608fd7c828c13168c46a5c81fbf400275ac","datavalue":{"value":{"entity-type":"item","numeric-id":1702897,"id":"Q1702897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$3AD955DD-0C47-400A-B50D-840309F95446","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05656618a7fbd87833428b51ffbb73b7b47e20fc","datavalue":{"value":{"entity-type":"item","numeric-id":4077431,"id":"Q4077431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$BD64F3B6-AD8D-493B-9728-7D94EF9D8065","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18533ee6a146cb79018cb77e7f9ebb7312adb2b3","datavalue":{"value":{"entity-type":"item","numeric-id":6651940,"id":"Q6651940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$7E54390C-F68D-46A3-94B6-44A16C304A87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"426e2dec292567619d8946d3b9c6e612c9eee6b5","datavalue":{"value":{"entity-type":"item","numeric-id":5310681,"id":"Q5310681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$F03F8C15-6B3D-4AEA-96E4-BCEFA2593397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ac557a679c59fc4a070eb3cbd75928e511a2612","datavalue":{"value":{"entity-type":"item","numeric-id":5883578,"id":"Q5883578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$2B257A9D-DF93-402D-8D4C-DA10F33F018D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1cc3e320a29fb63240b3b709fe5bc497385756c5","datavalue":{"value":{"entity-type":"item","numeric-id":6194570,"id":"Q6194570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$246C0240-727B-4E18-A86F-17EBE0ACCD48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2b799aade81b4cd5b689709b2689d4aca488326","datavalue":{"value":{"entity-type":"item","numeric-id":832229,"id":"Q832229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6938564$2CF17A51-611A-4E21-AD37-8AAFC44E6A52","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Predicate abstraction for hyperliveness verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Predicate_abstraction_for_hyperliveness_verification"}}}}}