{"entities":{"Q805251":{"pageid":807099,"ns":120,"title":"Item:Q805251","lastrevid":49512031,"modified":"2026-01-07T10:30:53Z","type":"item","id":"Q805251","labels":{"en":{"language":"en","value":"The existence of refinement mappings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4203737"}},"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":"Q805251$F19E6369-E797-48DF-BF8F-BD389116B2A9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ecbad9d1ac4942eb5ccc1f4893ea0c060073adfe","datavalue":{"value":{"text":"The existence of refinement mappings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q805251$EC838B4C-E521-452F-A373-BBEF99A0ADEF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"321c9b8cafcea17240698e0c01cf7078d5f9d18f","datavalue":{"value":"0728.68083","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q805251$E55633C7-0CAF-4584-9A2D-7A8D277B7435","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"55cbc41d3c802159a7d4e5e7b905e12cb4fa63d4","datavalue":{"value":"10.1016/0304-3975(91)90224-P","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q805251$1938BE50-FF40-42CE-90A7-964975DC7574","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f7720f013cde2512621480147576e51273a4c701","datavalue":{"value":{"entity-type":"item","numeric-id":265786,"id":"Q265786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$B6D555D9-216D-4881-A114-0B051AD8DDFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"209ba2abb9262ee2627b025b7dc9cc61471e318c","datavalue":{"value":{"entity-type":"item","numeric-id":661001,"id":"Q661001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$6E77AD28-7EC8-42C3-9AFD-6E4E5E50F0C1","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":"Q805251$50BB4C92-6DF1-4D47-879D-E25AB4673610","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"391107ffc7a24346d69c573e292e4ff4587e3aaa","datavalue":{"value":{"time":"+1991-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q805251$249D72FC-553D-402F-8D57-3B8B77ADE999","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1f9bc22f13af284a56e64b5d41521923958a1201","datavalue":{"value":"A refinement mapping from a lower-level specification \\(S_ 1\\) to higher- level specification \\(S_ 2\\) can be used to prove that \\(S_ 1\\) is a correct implementation of \\(S_ 2\\)- if such a mapping does exist. The goal of the paper is to find out assumptions about specifications to guarantee the existence of a refinement mapping.    A program is represented by a state machine (which may be infinite-state) specifying safety requirements (behaviour satisfies the property if it can be generated by a program); fairness constraints are represented by an arbitrary supplementary condition. A refinement mapping from a specification \\(S_ 1\\) to a specification \\(S_ 2\\) is a mapping from state space of \\(S_ 1\\) to state space of \\(S_ 2\\) which preserves state machine behaviour and liveness. Three cases when a refinement mapping does not exist are mentioned and it is shown how to overcome these problems by adding auxiliary variables (i.e. by adding internal state components not affecting the visible behaviour) to \\(S_ 1\\). The main result is a completeness theorem which states that, under three hypotheses about the specifications, if \\(S_ 1\\) implements \\(S_ 2\\) then one can add auxiliary, history and prophecy variables to \\(S_ 1\\) to form an equivalent \\(S_ 1^{hp}\\) and find a refinement mapping from \\(S_ 1^{hp}\\) to \\(S_ 2\\). Some examples demonstrate why these three hypotheses are needed.","type":"string"},"datatype":"string"},"type":"statement","id":"Q805251$32EA897E-E5AB-4DE7-B619-39E239E4A4FF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q805251$20E63CDB-63BE-4440-8172-11CC287AEDB9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be135996bfe01f4cff335d8af9081e136b173819","datavalue":{"value":"4203737","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q805251$0CDC0BDA-A01B-40A3-8449-D0E54983EA0A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f9ac4ef6ef6c5f8856ee80195276e724e0b6225a","datavalue":{"value":"correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q805251$FA4C19E1-EF8E-49A2-AD6F-1DC15E4F49DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d584e359576a00f85def0b98465ac7707c1c7959","datavalue":{"value":"safety","type":"string"},"datatype":"string"},"type":"statement","id":"Q805251$234F38A1-ABB2-40E0-9ABE-9177DE364ACE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47511de611e7ca7c7f052290389ebfdae4c32892","datavalue":{"value":"specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q805251$27636531-87A4-43FF-BB00-E5B8977FBCEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0f43b5d8c0ae8848835abc81341e946063dd5eca","datavalue":{"value":"liveness","type":"string"},"datatype":"string"},"type":"statement","id":"Q805251$D2327865-1DEB-4968-B8E8-BEFF9F74706D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5463dcc3cbfbf13733252c4b89f648bd569a84f4","datavalue":{"value":"refinement mapping","type":"string"},"datatype":"string"},"type":"statement","id":"Q805251$F8C5E05A-9556-4256-99CD-97BC11E3AD71","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"90e834492c280ea6f7cd09939cbb51910bf38c22","datavalue":{"value":{"entity-type":"item","numeric-id":1006888,"id":"Q1006888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$99C4C34D-7D32-4CAF-8ABC-2C7D7A08510B","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":"Q805251$F1F3DA62-CF11-4C1A-83FA-BF2B93616726","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2c57dfd81934c0c76c7925c937211e00638a6bf","datavalue":{"value":{"entity-type":"item","numeric-id":1100884,"id":"Q1100884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$CD33DBB9-7925-4E5C-986E-B552404BA324","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc6482fda869c7df0ed32fd6ade8f790a1ff04cc","datavalue":{"value":{"entity-type":"item","numeric-id":5585020,"id":"Q5585020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$D0E02FCE-284B-4D66-BB8C-90796F1E7ED3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e33b53c9004b61a90401a2052769d8efa2f34a0","datavalue":{"value":{"entity-type":"item","numeric-id":4120115,"id":"Q4120115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$C960DCBB-CC0B-4DEB-B5E7-A971838A3ACE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d21cbd0c791f083ee08a1e9e48b64281b87bb07","datavalue":{"value":{"entity-type":"item","numeric-id":3664404,"id":"Q3664404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$2D4C8AB6-0B10-444B-970F-2D0B4B195E26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb00c4a962f9e99ef72cf5ad5e884b86cfb17e25","datavalue":{"value":{"entity-type":"item","numeric-id":3345755,"id":"Q3345755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$6A6CE8EE-526A-4976-99B7-5B6C2A85C505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd2791da5b87f3897ecd063b68e70aea276f020b","datavalue":{"value":{"entity-type":"item","numeric-id":4178461,"id":"Q4178461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$2E68EEED-579A-4A26-86BA-F6A345A91E65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9b10461a4b1c31290683122ca9de274288aa8e1","datavalue":{"value":{"entity-type":"item","numeric-id":1095649,"id":"Q1095649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q805251$9C7053DF-5F0A-4D7A-A7DF-2333FD787DB0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9b28939484a45a5954bda01b8221e87a8f32cc35","datavalue":{"value":"https://doi.org/10.1016/0304-3975(91)90224-p","type":"string"},"datatype":"url"},"type":"statement","id":"Q805251$DF4B8B13-884B-4266-946A-83F13560E9F7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5235ab2e9afad80c9a03eabea87ef208b5014962","datavalue":{"value":"W2132107743","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q805251$35C705D0-6AAA-4187-8120-04303E85F184","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce179260ab0ff47ebfaac8a048ddf1066fa268ec","datavalue":{"value":{"entity-type":"item","numeric-id":3713577,"id":"Q3713577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c127a8a97bb7f75e1bdd82962cbd019b4c3ec2b6","datavalue":{"value":{"amount":"+0.7849467992782593","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":"Q805251$2031C04B-228B-40C7-813D-7722F474BB6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa9eaf47ad74c5b6613c305fd1ead4bf479fab31","datavalue":{"value":{"entity-type":"item","numeric-id":4522331,"id":"Q4522331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8bf91734a6dac9dd995162f5326c4b14ddc6e06","datavalue":{"value":{"amount":"+0.7805635929107666","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":"Q805251$25FB481D-8C3C-4519-8A41-FF4F0DFF0DE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"245728ea1091b8b8a2c7dfe7ed8eb6ec3d7996aa","datavalue":{"value":{"entity-type":"item","numeric-id":5403461,"id":"Q5403461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"679971765df4b8667fa59332052a9a62c7b87dac","datavalue":{"value":{"amount":"+0.7748193740844727","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":"Q805251$7DB15078-1513-4C9F-9DCB-7847E0FE290B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26567cadd41c1aaab451386b3d466d03d8f9c59a","datavalue":{"value":{"entity-type":"item","numeric-id":1323314,"id":"Q1323314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"619ad4103e590937ae9305fc0cb2fb64fe575026","datavalue":{"value":{"amount":"+0.774298369884491","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":"Q805251$EDD6B31C-FA14-459D-B8DD-F2D679181DE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9546ecc581a57aa727cf7de31e001286230e40eb","datavalue":{"value":{"entity-type":"item","numeric-id":5897075,"id":"Q5897075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7676bada5cfce144c33e5d9dd23de1a55dedbc18","datavalue":{"value":{"amount":"+0.7715093493461609","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":"Q805251$F8DDDA26-9709-45B7-A518-71EA2B81842E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:805251","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:805251"}}}}}