{"entities":{"Q1112588":{"pageid":1123337,"ns":120,"title":"Item:Q1112588","lastrevid":69672183,"modified":"2026-04-13T08:36:52Z","type":"item","id":"Q1112588","labels":{"en":{"language":"en","value":"Semantics and verification of monitors and systems of monitors and processes"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4078765"}},"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":"Q1112588$41D82B70-8BD2-48CF-B0FE-F133BFD50BF2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"85ccbea1ada690e3c770dea6f89a990e2df78498","datavalue":{"value":{"text":"Semantics and verification of monitors and systems of monitors and processes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1112588$C787DF39-DDC8-4B10-BE41-68E4B4E2CEEF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c6ce4c5e074636acf4aa7fe4f03544f38881ef41","datavalue":{"value":"0659.68022","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1112588$898E9381-F572-48DE-83F1-3B97447B2E5E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"44a8189cd801be9b393e20f75ac0396b6e2be873","datavalue":{"value":"10.1007/BF01872845","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1112588$A8C57721-8C79-4D74-8225-2A86B67DF138","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8b12b0efa1b6f27c7b983f7b3e41b4f5f7cbb272","datavalue":{"value":{"entity-type":"item","numeric-id":1112587,"id":"Q1112587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$7A32EF1A-5916-47F3-AB5C-7FE81C3B6BA4","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"57115b4722082b3277b4db3ad0412a8293b7033b","datavalue":{"value":{"entity-type":"item","numeric-id":251292,"id":"Q251292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$B66686E1-D1DC-4294-B744-F7211EF9D92E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"31a1937240ca4a323604b4728c31d242b5596d7c","datavalue":{"value":{"time":"+1988-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":"Q1112588$1169EE99-B0D8-40F1-84ED-F4F7AF1C74BD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f324c5e85d3ea5e172dec57a8d1d155430d94eb7","datavalue":{"value":"We present a sound and complete semantics for the monitor concepts of C. A. R. Hoare. First a method for specification of monitors, introduced by O.-J. Dahl, is reviewed. This method is based on the relation between the historic sequence of monitor procedure calls and the historic sequence of monitor procedure exits. Based on such specifications and our new monitor semantics we present a method by which it is possible to prove that a concrete monitor is an implementation of an abstract one.    In the last part of the paper an axiomatic semantics for systems of concurrent processes and monitors is introduced. The method supports verification by separation of concerns: Properties of the communication to and from each process are proven in isolation by a usual Hoare style axiomatic semantics, while abstract monitors are also specified in isolation by the method reviewed in the first part of the paper. These properties of the components of the system are then used in a new proof rule to conclude properties of the complete system.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1112588$DA66171B-7E0A-45AB-9560-32331B4282AA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1112588$C05F0678-42CF-4BC4-8D6E-A1F5D3874A76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec3769495799f08479987ac368adf64f125a2b66","datavalue":{"value":"68N25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1112588$20E5CF2B-47AD-4CA4-A82E-5C95C00475D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1112588$73C1019A-CBD9-47F2-B833-AEB3E4780AFA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a98865ae38f86fc03bbd70cffde3a7db4be989d5","datavalue":{"value":"4078765","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1112588$7423C9C6-1268-419C-B847-1465FEB9C772","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1278eca63e6491eb6b3543fcc42d91871bdcfaf0","datavalue":{"value":"specification of monitors","type":"string"},"datatype":"string"},"type":"statement","id":"Q1112588$0A174DDC-E5BF-4265-ACE1-4B31C21854ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"533247662bdba5627acc8ace2ce6a4ec5a2113cf","datavalue":{"value":"monitor semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1112588$4BFC8F3D-0748-459B-8D9E-4CB9D1536239","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c078ac6b4aa6494d6d5c36981e624a189730ba5a","datavalue":{"value":"axiomatic semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1112588$4698FD7E-5F9E-4500-9331-F791AB841D03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d0293c1324467179851225e65339530b673ab32","datavalue":{"value":"systems of concurrent processes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1112588$857A48E2-1D7B-4FDB-A108-C0AB021BC2D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"edc54e2ee713bf6ef933abe433da86dc03aec7ba","datavalue":{"value":"proof rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q1112588$068599A0-859A-4A9E-8C07-026050CD4E3C","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":"Q1112588$AD4FD500-BE68-42E5-A58F-DE8286274F99","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ec3996c14b206674e33c3ff3678191b3d324529","datavalue":{"value":{"entity-type":"item","numeric-id":3922144,"id":"Q3922144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$548F8778-0F25-4CDD-AEAA-2073D2EB7321","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3bc80122c3248b7370a66f915205122d19550f7","datavalue":{"value":{"entity-type":"item","numeric-id":3925144,"id":"Q3925144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$6A2CD1BE-8207-4167-99D6-DA8086391741","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$0873F04C-3F0B-4270-BD82-B68DD4A80E01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"590527b9ab06424671d175206ffd9142f16a79f0","datavalue":{"value":{"entity-type":"item","numeric-id":1112588,"id":"Q1112588"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$3DB6CF4F-E5F6-4881-A395-ABB2032B581E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$E6DE474D-AF1C-4CC1-8AC9-650D32572275","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db463348657cf41d5ff4d422c54e0c686e6e5dfc","datavalue":{"value":{"entity-type":"item","numeric-id":2554952,"id":"Q2554952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$D33339E9-0059-483F-8BA4-66A08E54B69F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3528a4c6aa7c1dbb75517b1e32592cd5687df0c4","datavalue":{"value":{"entity-type":"item","numeric-id":4066584,"id":"Q4066584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$D1AE565C-803F-43F6-9F28-C8AE293AF0C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b0f593aaa3110f1e8f538d98538d65a9ad442a","datavalue":{"value":{"entity-type":"item","numeric-id":3777424,"id":"Q3777424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$77CFD8EB-19C0-4F70-B5DC-1D0AE6D9FE13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acc5be8d059ad8416fab0a58a60f13f89930298a","datavalue":{"value":{"entity-type":"item","numeric-id":4085227,"id":"Q4085227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$D8F7668C-2790-4191-8031-3CDAC3AC5FB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68d7877f5c06b692012bb89ac63c690d31fa44f3","datavalue":{"value":{"entity-type":"item","numeric-id":3942371,"id":"Q3942371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$5D7848F4-36CF-4043-9A40-BE2C6CC6CBCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b524155ca812bee0e1b7f8a0a6113b4062250caa","datavalue":{"value":{"entity-type":"item","numeric-id":3330490,"id":"Q3330490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1112588$CC69B71F-44EB-4DAF-A0E8-FA8498533BBB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3206540081d005e1a1972800134291ffb6737b1","datavalue":{"value":{"entity-type":"item","numeric-id":4727411,"id":"Q4727411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ab30d97ad206a6f6ab89a9cacfee6036232d8c4","datavalue":{"value":{"amount":"+0.8288118243217468","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":"Q1112588$EE7D911F-46E7-4B30-AF3F-272E9E972628","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"152057a1f33cf8ef65f6e795e36cc8e54718dfe5","datavalue":{"value":{"entity-type":"item","numeric-id":1077155,"id":"Q1077155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c0271d60ed4e3286ecc9cb5f096c5e6807246ef","datavalue":{"value":{"amount":"+0.7683887481689453","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":"Q1112588$8EEA5F32-65CC-4CDD-A4D1-697B52354F52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20a03ee5f4fed6653ba05bc7108abe53a186a09b","datavalue":{"value":{"entity-type":"item","numeric-id":3700806,"id":"Q3700806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ce2a49628c41d5f650d3ccbf604f9c827d348b5","datavalue":{"value":{"amount":"+0.7526667714118958","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":"Q1112588$B9E33ACC-A827-4DF2-A391-AF69A0DE0F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c6f994329fed0f753fd3a9073563a9a9b20a737","datavalue":{"value":{"entity-type":"item","numeric-id":3680251,"id":"Q3680251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb369b450e821afe0f33b135efab0aa7fa6fc0e2","datavalue":{"value":{"amount":"+0.7466259598731995","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":"Q1112588$86446908-A52B-4638-8FBC-68BA50CD84AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc49e0b590d7de5a445751974dbf0997413a7183","datavalue":{"value":{"entity-type":"item","numeric-id":2811337,"id":"Q2811337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c52392782cf43fdd021f8c60c1b6ebcfcfb6d80f","datavalue":{"value":{"amount":"+0.7446759939193726","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":"Q1112588$1CFEF122-2560-4F46-8436-B4D24487C109","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Semantics and verification of monitors and systems of monitors and processes","badges":[]}}}}}