{"entities":{"Q2842001":{"pageid":2852721,"ns":120,"title":"Item:Q2842001","lastrevid":51784844,"modified":"2026-01-20T00:46:56Z","type":"item","id":"Q2842001","labels":{"en":{"language":"en","value":"Reachability for finite-state process algebras using Horn clauses"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6192845"}},"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":"Q2842001$1BED5B0F-DDF4-46EC-90C1-BAC1AB515EB3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6cbcca0fbd10206ae42db10a48fea49124e7cb46","datavalue":{"value":"1295.68169","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$3692A7A3-EAE9-40BB-8B5C-55885E57AB58","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"324a3b441b4ff6abcae93bf5e1ee893e0ecd8d30","datavalue":{"value":"10.1142/S0129054113400121","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$E773F042-6C22-437C-B341-6C602C8DBA40","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5deb182e107e834f68ef7a93841d825a137a5b6a","datavalue":{"value":{"entity-type":"item","numeric-id":444501,"id":"Q444501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2842001$1D4EC2F6-8F3D-41AD-A396-971BB53B5011","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"66b9832b777d3d49331312d3eb8a93c8014d39e0","datavalue":{"value":{"entity-type":"item","numeric-id":444502,"id":"Q444502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2842001$0758B53D-4EC4-43C6-96D8-FE3686B05D79","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"47adaa7123c6f3744cf7fa8eab088d52b4982295","datavalue":{"value":{"entity-type":"item","numeric-id":2703009,"id":"Q2703009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2842001$00A99882-A95D-4EAA-9052-1D4197270179","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c86eeb1cf1b5bc0e7bda48e7a87fbb18b6ccc2d0","datavalue":{"value":{"time":"+2013-07-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":"Q2842001$DD2CC8E5-9AFF-49D0-BF80-B33C9C1D3E5E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$DA62E104-945D-4658-A2B8-8542DB1303EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$A0455D8C-700A-4999-AEBB-203B7586DA05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$A7AB3FE8-26EA-4645-BB45-199653794307","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c36d6b2470873b409616acd230a5090ab1b17def","datavalue":{"value":"6192845","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$68B7819E-4197-44D9-BDED-E2DDCA2A0318","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a618b40b0e1c60d8f3695a0363009e29e3d436f0","datavalue":{"value":"reachability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2842001$505EB225-B7C3-4F1C-9E31-AD9B3C80CCB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fef6478deebea6192a3423f56cbaa462613b7716","datavalue":{"value":"process algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q2842001$21D08111-6B23-4970-8152-2CDF10A63088","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dca5cc682e76d80a491afdf82202532c8173882c","datavalue":{"value":"static analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q2842001$9C32428D-397B-4D90-B9F9-A4B6395F2ED1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e431190495251d75e7d7f973ca704f4139885eb","datavalue":{"value":"Horn clauses","type":"string"},"datatype":"string"},"type":"statement","id":"Q2842001$E1CC3A03-6CEA-44BA-9D79-D1E4284B07BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb1658b60e766a02ebffc17e47bf24ae50d17b7e","datavalue":{"value":"CSP","type":"string"},"datatype":"string"},"type":"statement","id":"Q2842001$AECEE364-FBC8-4A71-A9D7-573D793ED4CA","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":"Q2842001$3E2758D8-51FF-4FB8-AC72-9ECC381BDE08","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"624ebda7f485233c072e73ea011eff708305b483","datavalue":{"value":"Q51540658","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$13FA5F84-F825-4AF8-AC3F-22C1D15F1A72","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"21e625f666bcde7c93c8d1941da0c32e6b521acc","datavalue":{"value":{"entity-type":"item","numeric-id":444504,"id":"Q444504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2842001$302A9944-E470-447F-AFF8-66A5A333839D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4526d3bdd4ed025df8cee996f0066239af013785","datavalue":{"value":"https://doi.org/10.1142/s0129054113400121","type":"string"},"datatype":"url"},"type":"statement","id":"Q2842001$8D9D2765-A4C7-4CD4-9E54-114DF7A84E62","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"997d63ecc0596483c1ea2f562b32add50ccd3d3f","datavalue":{"value":"W2101393622","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$AC84E9D0-23C0-4C66-B8DE-40F1098B8B96","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"d0846561f7f74dc54a2c39eb57d9c1f44af0dc02","datavalue":{"value":"journals/ijfcs/SkrypnyukN13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2842001$9D74E23C-265B-4A19-8CF7-9A93F327E02A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1aceb0ac87291086b05648b78f92e0d5d3ed2b32","datavalue":{"value":{"text":"Reachability for finite-state process algebras using Horn clauses","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2842001$86CA9575-940B-40D9-9204-ED54CB92AF66","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8738554c42f70b716a033fb85f2765eec4102d31","datavalue":{"value":"An algorithm for solving the reachability problem in finite systems that are modeled with process algebras (variants of CSP with some syntactical restrictions to ensure a finite number of states) is presented. The method is based on static data flow analysis; actions are equipped with labels which serve only as pointers into the syntax that make it easier to express the properties that are proved for process algebras. With the help of labels generate, kill and exposed operators are defined. The algorithm exploits a set of Horn clauses whose least model corresponds to an overapproximation of the reachable states. The computed model can be refined after each transition, and the algorithm runs until either a state whose reachability should be checked is encountered or it is not in the least model for all constructed states and thus is definitely unreachable. Only a part of the labeled transition system is built what leads to a lower time and memory consumption.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2842001$13D467DA-CB75-4CA7-A986-CC7E48FA3A1F","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"773908fafc294c05eb3467ec5d713b5469e8b7b3","datavalue":{"value":{"entity-type":"item","numeric-id":590927,"id":"Q590927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2842001$75B0826D-AA78-4FFC-B3E8-89747B15C2D1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"457316d914ac916a1a9a3ee4a091be9c5a9f2de9","datavalue":{"value":{"entity-type":"item","numeric-id":3172877,"id":"Q3172877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42971b0bc231fb28185a79ce1940b81070640b01","datavalue":{"value":{"amount":"+0.910702109336853","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":"Q2842001$4976B837-45D5-4EEA-B894-C5379C36C157","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3cb0a4260d6d19d98ea28f7aec373f4de828a5a","datavalue":{"value":{"entity-type":"item","numeric-id":5505595,"id":"Q5505595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ead6039a841f8e9da3ad1aca2e9876149f65ff68","datavalue":{"value":{"amount":"+0.7594025731086731","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":"Q2842001$2C9FABE5-D1E4-4A6D-9E5F-27628B9EA665","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c593662561f1d9f007b40aa183893b0c369c0fba","datavalue":{"value":{"entity-type":"item","numeric-id":5902412,"id":"Q5902412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2dc2ddb8d574fc622fc55ca620a3108ed70e6c89","datavalue":{"value":{"amount":"+0.72065269947052","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":"Q2842001$B329929D-02FB-475C-AD1C-9CC30C0EAEA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"adf1b52ebb85f2c0c60679f5a49de02fe6c6b895","datavalue":{"value":{"entity-type":"item","numeric-id":5191507,"id":"Q5191507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"802bd7e9c08baa34590184282249d13cd3b5519b","datavalue":{"value":{"amount":"+0.7086439728736877","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":"Q2842001$347F779A-4977-49CE-9B71-7531B4097658","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca0ce561ec9a25dd0f89095b4d05aba6cc03a1b1","datavalue":{"value":{"entity-type":"item","numeric-id":4610333,"id":"Q4610333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"632805681b9327b6e15d3daf7a694dcc5e2e06d1","datavalue":{"value":{"amount":"+0.7065562009811401","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":"Q2842001$1F16979B-1F63-47DA-89ED-5757C7516F23","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2842001","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2842001"}}}}}