{"entities":{"Q402129":{"pageid":403896,"ns":120,"title":"Item:Q402129","lastrevid":61623267,"modified":"2026-04-11T00:32:47Z","type":"item","id":"Q402129","labels":{"en":{"language":"en","value":"Efficient CTL model-checking for pushdown systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6334961"}},"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":"Q402129$2DC7CEBA-47A6-4D3A-9380-9B5F4795144A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dffbf35d8e72b557a3f6f393d75d5397bea5833c","datavalue":{"value":{"text":"Efficient CTL model-checking for pushdown systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q402129$9319E7E0-3B08-4DD3-88E2-49A6817CF77A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f4e949c9a6fdad60c0649344a5db0aa30acd2a7b","datavalue":{"value":"1360.68599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q402129$3E175CE2-D327-4813-9A49-9693D47A9232","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7827c426fd62b1155223da4c43f3f5ddccba9caa","datavalue":{"value":{"entity-type":"item","numeric-id":342710,"id":"Q342710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$4D5E3DD8-8910-40A4-AB9D-A5F938DEDA6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4210cde0488918f9e758e0070524bd78d3176514","datavalue":{"value":{"entity-type":"item","numeric-id":402128,"id":"Q402128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$91C5FA55-AC01-48A8-8DF8-6AC25CF0916F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$12B1E4B1-F109-41DB-9A0C-358D90A098BA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"839eced7df0c4a631ff6c9629b85502b0309c881","datavalue":{"value":{"time":"+2014-08-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":"Q402129$359D04D3-27EB-4536-B301-E5907402ACB2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q402129$6EBC231A-E129-4DFB-924B-99CB37C08B90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q402129$0B8E0E66-9A97-4895-AAB0-465DDFAD267B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q402129$B4432FCD-006E-4115-B9C2-264F500A014D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6117a8d2c1a0c14bd17e72754a2a4f82c9273abb","datavalue":{"value":"6334961","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q402129$C339F5B3-BAA3-4952-830A-CE64056C7E8A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a0472569160d89698056e160debeeb3d577e82c6","datavalue":{"value":"pushdown system","type":"string"},"datatype":"string"},"type":"statement","id":"Q402129$3E6AB789-133A-477D-837C-4E67C0D73744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"379a567f0f983e236f95705804d342510fc41004","datavalue":{"value":"model-checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q402129$D1160BF8-2E42-418B-8D9E-C215B60D1732","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af948ab56df44408fff2ba197f928e63c9954960","datavalue":{"value":"CTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q402129$7EC57401-9BC0-473F-B67B-900EB7403AD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bbd733c3f6badf4366ba1faadb69c250de8dfec1","datavalue":{"value":"CTL with regular valuations","type":"string"},"datatype":"string"},"type":"statement","id":"Q402129$3CABF292-0962-4BBA-8837-FFACF8151E14","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"22220ec2b8401d9dd83d45be7c63cb89261ff117","datavalue":{"value":{"entity-type":"item","numeric-id":5975094,"id":"Q5975094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$4C6BE697-D59C-4347-8CC1-17CCFC6B7D2E","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":"Q402129$F310F407-4A0C-4DBA-8C86-C3F0B7C3B9AE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e6e5f96f0bb1aa6346bf5b9ac097039467dd580e","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2014.07.001","type":"string"},"datatype":"url"},"type":"statement","id":"Q402129$CC0C953D-861A-4EFD-8A52-20EDB9C497F8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4acfc43a85e73f3aca8b0d8bc29e5419a2d7b378","datavalue":{"value":"W2020438328","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q402129$A54C5E32-F7F6-44D5-8972-699E62B6CED0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"59ebc8c6731a9ba8b7c88fd686053c929a1ba298","datavalue":{"value":{"entity-type":"item","numeric-id":4551162,"id":"Q4551162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$96DBD9CA-72D0-4553-816A-BB1FF0078EC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54e7a108370169c16838733bc613c6abdf38f709","datavalue":{"value":{"entity-type":"item","numeric-id":6044114,"id":"Q6044114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$44742D56-69CE-4AEF-8282-EBEDFB704A39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a133b2b9476ffc4401b56d83bdfd1f487592e7be","datavalue":{"value":{"entity-type":"item","numeric-id":2754086,"id":"Q2754086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$B1FCB456-3788-4B7D-ACCD-A28B2663B3C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f383fb92aa2cccd41635d3cc5fa0ca5c0c6182c3","datavalue":{"value":{"entity-type":"item","numeric-id":3587257,"id":"Q3587257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$E239DBFF-DD00-4862-869A-143BE2EAB05C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34c9f9c418382824d2175732eb97c5ec8a5259b3","datavalue":{"value":{"entity-type":"item","numeric-id":2373715,"id":"Q2373715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$A5F50680-DFE3-4E83-99FC-E23879296B18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1dc6aedd9ac3c25d0a03730d5d12f05035842f62","datavalue":{"value":{"entity-type":"item","numeric-id":4571973,"id":"Q4571973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$75923FCE-AE8D-4ADF-AB61-01376C6F18D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2de91ecb193514088bc3752dcf7515e5158d8d0a","datavalue":{"value":{"entity-type":"item","numeric-id":2754072,"id":"Q2754072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$5BFA2911-F894-4425-952B-11D9B79D21CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ec39e0aae078ea86b2a7192e600175bfda00e3f","datavalue":{"value":{"entity-type":"item","numeric-id":5312916,"id":"Q5312916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$147B1EB3-54E5-43C8-AB41-30C6630B634A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ab8130d3aff9409c6a296190aadf3113874d3d6","datavalue":{"value":{"entity-type":"item","numeric-id":4428305,"id":"Q4428305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$446EC1F9-A9DC-4D9A-AE27-5D1E693580F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65ba6ee4184d1e83b23af04ea3e34386770ce9f4","datavalue":{"value":{"entity-type":"item","numeric-id":4472439,"id":"Q4472439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$51831E30-251F-4D0F-B950-772AB16376FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b14d9eabf063c4fdd0e32a8e0bccf5a26d189e4","datavalue":{"value":{"entity-type":"item","numeric-id":4847017,"id":"Q4847017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$95607B73-0303-4E22-B7AD-779EFB77A88F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e902457964a312a605389238232d33897eb4c84c","datavalue":{"value":{"entity-type":"item","numeric-id":1887158,"id":"Q1887158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$1E632FD5-2347-40B7-B038-8338D1C93498","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85db71a32648e55138733c05985bbfe8ecd51d5a","datavalue":{"value":{"entity-type":"item","numeric-id":5714447,"id":"Q5714447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$6EF09322-8AD8-4C8B-A356-E397F38DB753","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44e1fc18aa850bac20ad3e82fe71d0c5870a03b4","datavalue":{"value":{"entity-type":"item","numeric-id":532393,"id":"Q532393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$B0E98DBA-E764-4591-AC9E-D2537A2FD8FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e099c29cb4a85f55d1d4608c736de84d6a2daf0e","datavalue":{"value":{"entity-type":"item","numeric-id":4737201,"id":"Q4737201"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$D7549858-674B-4A84-BC83-6220D76F2B94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$2249D1F8-DCD2-4214-A768-30B052891EAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"363e3db19b9c332e46164580496bfb20391b489e","datavalue":{"value":{"entity-type":"item","numeric-id":3522906,"id":"Q3522906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$00ED3CE7-D890-46CB-A866-1A2D789CEB5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07cd204d3e61e3a929ece0ad83fde7b9ae4724b5","datavalue":{"value":{"entity-type":"item","numeric-id":1333263,"id":"Q1333263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$B4AA0B7F-60F2-4984-AD38-3BA46A380760","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fe76e7c7c69ea3113cfd37113ad36ccb294761c","datavalue":{"value":{"entity-type":"item","numeric-id":5387861,"id":"Q5387861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$E7DE6015-9188-4393-9C33-77D453BB454B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff6eb349a791ef34219aa97210664902e99ca1cb","datavalue":{"value":{"entity-type":"item","numeric-id":968362,"id":"Q968362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$DEFB2DCD-7ABF-4C71-B9D4-AAC7B44E47CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99d9546809dd8770c3877fc48d5c3ed987470c2d","datavalue":{"value":{"entity-type":"item","numeric-id":2842876,"id":"Q2842876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$85E9B57C-9AB4-464D-B985-36547A273F63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7351a5b1debd8b8e0510ccc8864beebebdf77168","datavalue":{"value":{"entity-type":"item","numeric-id":1007544,"id":"Q1007544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q402129$B388DB60-AA86-4849-A087-9DCDE2B4B280","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dda72dd0387d3080fec6e3fc15edf49e556b7f76","datavalue":{"value":"10.1016/J.TCS.2014.07.001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q402129$11D6D269-01A1-432A-BE15-1B4EE5C6B6E3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a81d05c5057fb055fd0b7b1806601a483097f486","datavalue":{"value":{"entity-type":"item","numeric-id":3090847,"id":"Q3090847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f5bad60f5d71e07f84653e70422d32de406082f","datavalue":{"value":{"amount":"+1.0","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":"Q402129$27F22358-0705-4F2F-8D39-7480D85C79B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e7db2e6c90798e3e7be3aa35f58d3f4a6a178630","datavalue":{"value":{"entity-type":"item","numeric-id":4472439,"id":"Q4472439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72693326d21bda0361705b4b5d65d976fd3aad72","datavalue":{"value":{"amount":"+0.9605656","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":"Q402129$2325FEE0-29E5-4C4D-86DF-8D4EA5C515C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a07577d90b863174edcdb7cdfdb8e6c4ab41bb1","datavalue":{"value":{"entity-type":"item","numeric-id":2754086,"id":"Q2754086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8519480ca6cfbb7b5f353041c848085e41114ca2","datavalue":{"value":{"amount":"+0.9404959","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":"Q402129$66A05C97-8C12-404A-AE0B-A351545965A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d672bc119c6f2601b0011fccb9bb2bab36dfaab","datavalue":{"value":{"entity-type":"item","numeric-id":5883578,"id":"Q5883578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f5b295d1012926cbdc876e2d7998a5dd084eb62","datavalue":{"value":{"amount":"+0.9189664","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":"Q402129$ACD0E621-7F60-4A78-BFB7-74A93D75811A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72b7928ee93f953cc266179fafb7ba3a8831ce06","datavalue":{"value":{"entity-type":"item","numeric-id":5756743,"id":"Q5756743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5c37468b3dc05cfe8f74c1058eafa09c5aa1b62","datavalue":{"value":{"amount":"+0.90950954","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":"Q402129$D94A627B-6A0B-451B-A80E-3A830D9FA2C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a29f104c062d810eb205c185094771add2f78107","datavalue":{"value":{"entity-type":"item","numeric-id":2901199,"id":"Q2901199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81e647476e5cbffcc2358b3e4ec18c960b0ab34e","datavalue":{"value":{"amount":"+0.90406895","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":"Q402129$95FDAA40-25FC-4524-ADC0-297E2B842BDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c71f6edf2b4428d82cf29c2a351497cb1ae8655d","datavalue":{"value":{"entity-type":"item","numeric-id":4928504,"id":"Q4928504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81348237d57c91ca7644cb53dc017ecfe330eaff","datavalue":{"value":{"amount":"+0.9011764","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":"Q402129$3805D432-1E52-4DC7-8CE8-CE999F9893DD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Efficient CTL model-checking for pushdown systems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Efficient_CTL_model-checking_for_pushdown_systems"}}}}}