{"entities":{"Q685107":{"pageid":686956,"ns":120,"title":"Item:Q685107","lastrevid":47188321,"modified":"2025-12-31T23:06:08Z","type":"item","id":"Q685107","labels":{"en":{"language":"en","value":"Compositional checking of satisfaction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 417066"}},"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":"Q685107$07B9A072-EE80-43E2-8A80-525A20CA1273","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3018d848e12348cb2011aea0537d33ee310c5587","datavalue":{"value":{"text":"Compositional checking of satisfaction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q685107$01B5AAF1-A2A7-4EDB-B089-24C9D874D366","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a8d5303c476e367c3a32dab117294e77e12394d9","datavalue":{"value":"0776.68083","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685107$5D8E3009-17FE-48C3-80A7-FBAC165C0B3D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c6757236ae6ebd4346db2ae65c8253204895068b","datavalue":{"value":"10.1007/BF00709155","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685107$89A61E5E-251B-43EE-B9EC-C5FA9CECD8FC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc14b91f3ea67d454f18e791d265c69e1964e48c","datavalue":{"value":{"entity-type":"item","numeric-id":169903,"id":"Q169903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$4C5762AB-7596-4F28-A47D-F31E8BCB27D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a31faab77501481f5eeb576293dcd59bdbba3a61","datavalue":{"value":{"entity-type":"item","numeric-id":265794,"id":"Q265794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$F78BA9DA-6A40-434F-B92F-F74A634C8893","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":"Q685107$CE8FE188-64BD-4AA6-AA7D-E55577C9D8D5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"45eae072dc2fde41ae8741e47d8a8d06eb2b2f63","datavalue":{"value":{"time":"+1993-09-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q685107$E923EC07-FF76-4DC9-BB2D-D8C34F92F11D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3d7d9e4e75a900a55ac891b89681817ac5b64fa6","datavalue":{"value":"The paper presents a compositional method for deciding whether a process satisfies an assertion. Assertions are formulae in a modal \\(\\nu\\)-calculus (the dual of the modal \\(\\mu\\)-calculus), and processes are drawn from a very general process algebra inspired by CCS and CSP. Well-known operators from CCS, CSP, and other process algebras appear as derived operators.   The method is compositional in the structure of processes and works purely on the syntax of processes. It consists of applying a sequence of reductions, each of which only take into account the top-level operator of the process. A reduction transforms a satisfaction problem for a composite process into equivalent satisfaction problems for the immediate subcomponents.   Using process variables, systems with undefined subcomponents can be defined, and given an overall requirement to the system, necessary and sufficient conditions on these subcomponents can be found. Hence the process variables make it possible to specify and reason about what are often referred to as contexts, environments, and partial implementations. As reductions are algorithms that work on syntax, they can be considered as forming a bridge between traditional non-compositional model checking and compositional proof systems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q685107$A14FF342-C739-4AD8-A190-E48DF019820F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685107$EA73C525-0CD0-4F0D-9100-25BA14ABAB8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685107$AF1179DF-5F73-499F-9E0E-B53B16F91607","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685107$D25823DF-578C-42ED-8BFF-BFADE20A1FAA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"60f15773b64c1d696617e56b8ea17fce1d7e378e","datavalue":{"value":"417066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q685107$A385BF71-AF19-48AB-BC2C-212ACBCFD3E5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"000cae892649b86c08dfd4faa170d21befcdc840","datavalue":{"value":"process calculi","type":"string"},"datatype":"string"},"type":"statement","id":"Q685107$DC86942B-CC8B-45B1-9871-C7674B91A3AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6dfba264ed923dd13e3004a251bcdab07ddaa86e","datavalue":{"value":"compositionality","type":"string"},"datatype":"string"},"type":"statement","id":"Q685107$BFD76799-E067-41C1-8862-4EDBD1CCC534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26c4403d5fa8d9102bcd88ec8de73f9befa0d5ea","datavalue":{"value":"modal \\(\\mu\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q685107$71CEDBDE-DA5A-439E-A774-FA01FDAD1B11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q685107$A1A21E60-E513-4848-AFEE-9D64F02C0749","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":"Q685107$23F1CF24-C342-4CFB-A708-F6B58F623D6F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"23e6a970ef833d1f16c56166519e7e5cabfc785e","datavalue":{"value":{"entity-type":"item","numeric-id":1325848,"id":"Q1325848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$91930AA0-7ECC-4553-BB19-642D7E7D1E87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"731fff832e7711198e063399154f72f88c50c123","datavalue":{"value":{"entity-type":"item","numeric-id":3719811,"id":"Q3719811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$910B072C-6BE6-4E7E-9000-3F7CAEF7A5F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03e4c3801010a4bee6d03ee81a6a1a5d94252213","datavalue":{"value":{"entity-type":"item","numeric-id":3792217,"id":"Q3792217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$73008F17-12DA-4B43-B035-2AB6A5DADBCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1046b50af51c3932f3f883ecb7513f98f95e421c","datavalue":{"value":{"entity-type":"item","numeric-id":3033311,"id":"Q3033311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$DEFA2E83-A177-4543-BC75-CAD1A2A0D483","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c4261c45eb0bdc31b98abbe6dbdb3be8211dfa8","datavalue":{"value":{"entity-type":"item","numeric-id":1122572,"id":"Q1122572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$95BDBDCE-377B-4406-9C69-44E31CC95945","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6720ea54e8d7bda1f526d6d3b9396cc0b55a891","datavalue":{"value":{"entity-type":"item","numeric-id":1115196,"id":"Q1115196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$0C61175A-05AA-4735-A3F2-7C58F20F732B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0236c27b44b1d5ff87db3c624b16ad39c44b9863","datavalue":{"value":{"entity-type":"item","numeric-id":4038716,"id":"Q4038716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q685107$9F5A0AAC-40EA-4425-85FA-ACA77C13DB6B","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":"Q685107$69D57718-0753-4F97-BFEF-1106B12D4593","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7094a3c988c734ca21ea53bc6ec6f202282d2855","datavalue":{"value":{"entity-type":"item","numeric-id":3204034,"id":"Q3204034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"affde452f975cbcce7b09a45e4818805aa226d9e","datavalue":{"value":{"amount":"+0.7794543504714966","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":"Q685107$FBBB2B22-653E-45BB-8257-F53E9D31C0E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec14e4901ea245bd8ce158b1e1e23774b01fe852","datavalue":{"value":{"entity-type":"item","numeric-id":4511273,"id":"Q4511273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf1a5aaf14dafbda2d476e888b340e6ed71e9bc1","datavalue":{"value":{"amount":"+0.741706907749176","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":"Q685107$4429FDF9-8C89-4ECD-BFDC-D2885900949B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f74a4554d915abf3dc2af47a650d41ea7cdc430f","datavalue":{"value":{"entity-type":"item","numeric-id":3795197,"id":"Q3795197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b0ac4a99149f28ac50cf8b60752b4bfc08921f9","datavalue":{"value":{"amount":"+0.7359561920166016","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":"Q685107$1ADAFDF0-E952-4F45-8E80-169305A94066","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"34331347e02d515e4ee0fe876e26206c374f5390","datavalue":{"value":{"entity-type":"item","numeric-id":3683529,"id":"Q3683529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"327c6c34e11a3cd9b3b12abc389eb52b900851ae","datavalue":{"value":{"amount":"+0.7358134388923645","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":"Q685107$8E7D8C95-91BC-4B2D-825B-2F2FF2171DF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f302cd13facf53850a3bebbe6513c94f032b4938","datavalue":{"value":{"entity-type":"item","numeric-id":4633153,"id":"Q4633153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cb89422102a6bd07ea2831436fa605a05a6b68f7","datavalue":{"value":{"amount":"+0.7352724075317383","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":"Q685107$CECDA18A-742B-43D0-9260-CFFF748C380B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:685107","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:685107"}}}}}