{"entities":{"Q5403070":{"pageid":7432644,"ns":120,"title":"Item:Q5403070","lastrevid":75490732,"modified":"2026-04-19T06:20:48Z","type":"item","id":"Q5403070","labels":{"en":{"language":"en","value":"Model checking TLR* guarantee formulas on infinite systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6273794"}},"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":"Q5403070$DAA694D6-A445-400B-A8C3-CDC5B4FDEA19","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"20eb9ffff69946e5525876a182063efd8dd20e39","datavalue":{"value":{"text":"Model Checking TLR* Guarantee Formulas on Infinite Systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5403070$BC0F3946-5E52-44AB-8431-EE7109CA0A35","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6d177592b9e198caca575828d9f19b581700c561","datavalue":{"value":"1407.68296","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5403070$2D3B1633-384D-479B-9363-E2DE0EA148CA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0518c906df113c92e70a3118ddf671aa965b6f59","datavalue":{"value":"10.1007/978-3-642-54624-2_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5403070$9B28642B-FB99-4A46-B182-9B1C16D81FCD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4d50e4ae74c4e03e7085ea8b0f513478341a75b0","datavalue":{"value":{"entity-type":"item","numeric-id":1990505,"id":"Q1990505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$648364DB-58D1-43DB-A91D-9F738D36F0E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"51d22396de3566f8539794488d7dec5aa12d5cd7","datavalue":{"value":{"entity-type":"item","numeric-id":816214,"id":"Q816214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$EC4C1798-D5F2-446D-9E34-5C7BFF2EDE68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cf075aaec86a3ce2575469311f0a5edc1faa7cd9","datavalue":{"value":{"entity-type":"item","numeric-id":816215,"id":"Q816215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$C875779E-FF01-4857-9CBD-84F6DD3EF970","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4df2f4bc2ffe4036b415b2ee5c20621445d90244","datavalue":{"value":{"entity-type":"item","numeric-id":5403065,"id":"Q5403065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$9995C249-E088-4C5F-AE32-F485DAD930D5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"dffee03b61d790552fa728bec5833993c2eb4588","datavalue":{"value":{"time":"+2014-03-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":"Q5403070$687882B0-3FD8-460B-BC38-AE0DAECF339F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"831d6031784a91408bc0da6659d6bc2f185397c7","datavalue":{"value":"https://eprints.ucm.es/22647/1/master_thesis_-_two_sides_-_for_printing.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5403070$75F2F461-33EE-444B-B691-BF86C42E124F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5403070$A48E2335-1566-47D2-BA66-084407A23B9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5403070$2A7EB2B9-491F-4002-AD32-9583DEC017CE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"78bcee4ebe47968fb93337b5e2dcf030f9a56cb2","datavalue":{"value":"6273794","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5403070$A16B72BD-5B2E-4045-879A-9275FD2D26CC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b0be45dcf28f014d73413c8c1b0a2751733f815","datavalue":{"value":"infinite-state system","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$06AA78F3-4568-436B-89C5-3F54AFBF9AE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"302e7bd67d2646d1e0615c1195ca61ad56775360","datavalue":{"value":"rewriting logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$F5120BC1-B164-489B-ACDD-78DAC96838AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7837ca7b4ed6a21f47990cc2562459286134de64","datavalue":{"value":"Maude","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$2A38B4EC-0CA4-400E-BBF7-219FD676C155","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$1D2866EC-DF77-4051-94A5-B273BF21CFE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d1f39b31643ac956a3480ce4ac11bdca9d075198","datavalue":{"value":"strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$27F1A080-3392-481D-AE7B-14CCD508AC46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$3CB7DEBB-67EF-42A3-94DA-C31713F7B3E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba005853b00ddf56ecfb84cfed45a0d63e79bed3","datavalue":{"value":"TLR*","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$9D8B717C-E351-4531-9723-2E8DC2D8E161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c9c2c7b7154b47ca98fcd9cb94bddad93313dc2","datavalue":{"value":"guarantee formula","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$0BCC9C8A-AD77-48AF-B98A-BBF7186BD855","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a9ed6cf8b50d2b81691b7a80850da2327f5e980c","datavalue":{"value":"cache coherence","type":"string"},"datatype":"string"},"type":"statement","id":"Q5403070$ECB70335-87CC-4E0C-81A4-BB9871AADCAF","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"a819f4bec1fe057f398e273e4bfc43854e5ea7f3","datavalue":{"value":"Q123905825","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5403070$9E44A897-EDC9-46EB-8CF7-DE5AE3F19E7C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$4EA66685-05A5-436C-B90D-3B26EF77C172","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":"Q5403070$765D7A98-38B2-4C0C-B454-CC1856366115","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f8e3d9db4c663fb47d186ea593ce0ecc3f3e250a","datavalue":{"value":"W1508941494","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5403070$C4A1548D-7B1C-4B86-A5F4-568E1D0D77AC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"00e7fb512c3c2088a0e31db09a35588d6ca50ae7","datavalue":{"value":{"entity-type":"item","numeric-id":2958376,"id":"Q2958376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$E0D88520-8F9F-4AE4-B997-B29E23D4A209","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ac1705eaf70f76f225913c7cf0f442d5b7951ae","datavalue":{"value":{"entity-type":"item","numeric-id":4933287,"id":"Q4933287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$555E70B2-CDA5-4B21-A739-3A40697D3FFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb6701311971a6968fadc620d5e7ea9a2886adeb","datavalue":{"value":{"entity-type":"item","numeric-id":3164834,"id":"Q3164834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$24919233-B8BB-4254-9B87-D160471B2CF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b29867ca33fd9495ec2ddeae47f6f8c992f79cc","datavalue":{"value":{"entity-type":"item","numeric-id":5166636,"id":"Q5166636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$DC38A480-A1FA-4408-ABFB-5C2FCE96502E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b84e50d5b8107ff3d8511662cf6eee9934348f6","datavalue":{"value":{"entity-type":"item","numeric-id":1608914,"id":"Q1608914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$7F6CD577-7754-47B0-8455-58A9B478AA46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84ab5e8e2cb4633034d3747a964aea829975e001","datavalue":{"value":{"entity-type":"item","numeric-id":2503334,"id":"Q2503334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$2AE616D9-A811-454C-9DEF-51406F195706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69bd394a77de6a66e7c3ead14354e268bd49cc00","datavalue":{"value":{"entity-type":"item","numeric-id":997833,"id":"Q997833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$2D94C073-C54A-4F48-B191-FE070B0D7420","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c884171bba72c2b3f8a55330fd6748a3e548c6f","datavalue":{"value":{"entity-type":"item","numeric-id":5432339,"id":"Q5432339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$84C2E446-B994-4B17-B924-AA64D407C2A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c50fb2e1e8cf1b2f302165e38684d666bf1a4167","datavalue":{"value":{"entity-type":"item","numeric-id":5941101,"id":"Q5941101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$DA001406-6BF4-43E8-9086-49FDEA4A73D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf8ebc11e5152a7aaca233f3b6037de5f36fc738","datavalue":{"value":{"entity-type":"item","numeric-id":3766826,"id":"Q3766826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$159B7B5D-D7F4-4AA6-A248-8DA2F5DF67D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c264d0378a5f30df399a3e5c6ab315df59ddacaa","datavalue":{"value":{"entity-type":"item","numeric-id":1190488,"id":"Q1190488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$A5AA52DD-58B3-496E-859C-6F8E16D9E982","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d3f22f1e7ec73ba657b43cbe915c5d1ad1a36dd","datavalue":{"value":{"entity-type":"item","numeric-id":944377,"id":"Q944377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$3FF7FA08-D508-4CFE-962B-C2392CD1771A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb64814c00476c1c6bda57ea158d42486c84afb9","datavalue":{"value":{"entity-type":"item","numeric-id":2841225,"id":"Q2841225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5403070$97477E22-4464-4FE6-94B5-794E45671106","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e866be9b5b9cc4fc80ed6878d8463b70348f92ac","datavalue":{"value":{"entity-type":"item","numeric-id":5166636,"id":"Q5166636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ddc764c65c59b24b85c613cbcfe848bafe149bb","datavalue":{"value":{"amount":"+0.7931218147277832","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":"Q5403070$361EB48A-0CD3-4130-B129-0CA3AD948041","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65f1386d26c8c22b090c8f1ac130f1e318ecd9aa","datavalue":{"value":{"entity-type":"item","numeric-id":2851053,"id":"Q2851053"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a15e41d79e914b8e121fe125f9a5b505e8de5da","datavalue":{"value":{"amount":"+0.777262270450592","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":"Q5403070$43E0AD3A-6EB0-4CCC-A371-F60FD80E2705","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"95f9f687a5297234e093a151d1c25779a08ca874","datavalue":{"value":{"entity-type":"item","numeric-id":2945133,"id":"Q2945133"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5cfee935a48e6a6ac0868a9e61c57646c117a5c","datavalue":{"value":{"amount":"+0.7759767174720764","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":"Q5403070$55AFE913-5503-49C3-92C0-8A258D70E1A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27368f7c2fe1e37e3d66c5ac92d0ccdb54dc9735","datavalue":{"value":{"entity-type":"item","numeric-id":4933287,"id":"Q4933287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"875cf44d395e766fc3feef68ce1f66c80bcc3870","datavalue":{"value":{"amount":"+0.7673400640487671","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":"Q5403070$42B4D236-6895-4661-87DA-3C0748DEDF2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"89864765938afbca7a5a9ab468fb862125d764c0","datavalue":{"value":{"entity-type":"item","numeric-id":4426386,"id":"Q4426386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a300de5fe094053f4284b93a9043fc9ad76dd863","datavalue":{"value":{"amount":"+0.7663426399230957","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":"Q5403070$E70AE7EE-D933-41BD-9586-CCEFC5835E7F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Model checking TLR* guarantee formulas on infinite systems","badges":[]}}}}}