{"entities":{"Q866004":{"pageid":867852,"ns":120,"title":"Item:Q866004","lastrevid":64971672,"modified":"2026-04-11T23:27:12Z","type":"item","id":"Q866004","labels":{"en":{"language":"en","value":"On decidability and model checking for a first order modal logic for value-passing process"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5128548"}},"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":"Q866004$D48D021F-0F66-432E-8178-E4B80CE2B9EC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"510ba295d0fe0bf58885e7fd5304ce7d6c82810a","datavalue":{"value":{"text":"On decidability and model checking for a first order modal logic for value-passing process","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q866004$F16D45B0-B2B8-4CAF-BA34-8D66E713A00C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"db1cd1ba75d0e5580907d41548c0858f24325aa6","datavalue":{"value":"1161.68592","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q866004$B3ADBEF2-4C57-49DB-B95B-C6B6D2E29809","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"94de73ba11fd12ead5ed80f57d9cc5c84570148d","datavalue":{"value":{"entity-type":"item","numeric-id":507947,"id":"Q507947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q866004$1F735B40-1E53-4BE6-BF98-93F4162F25F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"109a2c1db1a35b8bca53c181e382a5e53b01a8c0","datavalue":{"value":{"entity-type":"item","numeric-id":348725,"id":"Q348725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q866004$5AD7745C-52A4-4CE2-8348-471A49A08D8D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f98e7827e954b81f9efe2be64c5ae8ff8fac944c","datavalue":{"value":{"entity-type":"item","numeric-id":419702,"id":"Q419702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q866004$AC3C8D74-4740-47B1-951D-98CD0E6CF19E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b6a3b01ed43848088ad19bc3cf2f29651a0e98f7","datavalue":{"value":{"time":"+2007-02-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q866004$B5E40E0E-52D9-4287-B133-896CB09D34ED","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cab927a1b6d3e0c2ce13bd31d04f6e520427aa4c","datavalue":{"value":"A semantic interpretation of a first order extension of Hennessy-Milner logic for value-passing processes, named \\(HML(FO)\\), is presented. The semantics is based on symbolic transition graphs with assignment. It is shown that the satisfiability of the two-variable sub-logic \\(HML(FO^2)\\) of \\(HML(FO)\\) is decidable, and the complexity discussed. Finally, a decision procedure for model checking the value-passing processes with respect to \\(HML(FO^2)\\) is obtained.","type":"string"},"datatype":"string"},"type":"statement","id":"Q866004$55A2C345-5268-411C-893D-ECDB125BF4E9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q866004$6E274E72-7092-4629-8F1E-5A9CDDA6BFB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q866004$1FFFB1A8-9BFF-4F4C-A832-4851ED79808E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q866004$25E99EDB-E1B5-41C8-B849-7C39C1605921","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"816f717ca2868401a722c698569e5041cd7c76ce","datavalue":{"value":"5128548","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q866004$C75F4DE2-33DA-4721-AFB1-F0BB1D4002C0","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":"Q866004$8AB97CED-17B3-409F-AC45-E45EE5A2217D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"db11469f5184274a9f6b9ec4cfa18d79f1bd9b35","datavalue":{"value":{"entity-type":"item","numeric-id":4222879,"id":"Q4222879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"44ae944d08277bd0673879b1ea6c4b2ba912c0fa","datavalue":{"value":{"amount":"+0.7936976552009583","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":"Q866004$18F2DBB9-DAAB-4586-B318-2F1067947DDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"963bb532a82c4d8a024c74d8826df7654fa373a0","datavalue":{"value":{"entity-type":"item","numeric-id":4364391,"id":"Q4364391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c91fd126a494c0de645b6016adfb23317a5e1915","datavalue":{"value":{"amount":"+0.7783566117286682","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":"Q866004$1AB4D2BB-A87C-4175-9638-62D63ECE3B5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bbae6fafa873b776d56141c1686ea0d10f5c1ef7","datavalue":{"value":{"entity-type":"item","numeric-id":1960419,"id":"Q1960419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c91fd126a494c0de645b6016adfb23317a5e1915","datavalue":{"value":{"amount":"+0.7783566117286682","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":"Q866004$AE688CA0-C452-4EFE-BE57-385D7009F949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07bfce2bd16a86af783d90e27947458b64b5d463","datavalue":{"value":{"entity-type":"item","numeric-id":1894680,"id":"Q1894680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"634b574d06d03eac4d7153bf9cadcbe0df3f4268","datavalue":{"value":{"amount":"+0.7694151401519775","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":"Q866004$7DF9D5E0-3417-457B-A7B1-5BCEF38E9FD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c625295057c013b440496ff426cfd998a2624415","datavalue":{"value":{"entity-type":"item","numeric-id":3457984,"id":"Q3457984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"023bdae82430ea578499a32454a9fdeb65b520c9","datavalue":{"value":{"amount":"+0.7678447961807251","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":"Q866004$C473EC1A-0CFF-405D-943D-9BA4380FCF47","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On decidability and model checking for a first order modal logic for value-passing process","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_decidability_and_model_checking_for_a_first_order_modal_logic_for_value-passing_process"}}}}}