{"entities":{"Q1920224":{"pageid":1930966,"ns":120,"title":"Item:Q1920224","lastrevid":47408287,"modified":"2026-01-01T16:11:02Z","type":"item","id":"Q1920224","labels":{"en":{"language":"en","value":"Decidability of model checking for infinite-state concurrent systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 918709"}},"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":"Q1920224$75A9FEB9-4CD2-437A-B68D-1FC4C457CBC8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"278df809e2d1a2873c90110ba9b49519d4278054","datavalue":{"value":{"text":"Decidability of model checking for infinite-state concurrent systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1920224$93AA22C8-9BC2-4176-AF00-1336D9F773D1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"01e87a751dbaec6f73c6e095b1fc10b044fa7bbc","datavalue":{"value":"0865.68046","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920224$0EDD6B1D-96A6-4579-95AA-759197F4F8C8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5e47b8a1818346ce22bd45f99ec3c619fd43a6a3","datavalue":{"value":{"entity-type":"item","numeric-id":264200,"id":"Q264200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1920224$D6826EED-D6B5-4256-9D35-753C13D47A7B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1920224$C78B103A-3B94-43C7-83B1-C4AEAFB0CA47","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1d09c5b0b415fa939fde0c7442de6e15f6267846","datavalue":{"value":{"time":"+1997-06-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1920224$FA24E9E9-A0E4-49BF-8971-7106C0B19D8E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e241069b895647ea110b1605430c6e13e6413f9e","datavalue":{"value":"We study the model checking problem for linear and branching logics and two models of concurrent computation: Petri nets and basic parallel processes. While Petri nets are a rather powerful model, which can be used to represent and analyse a large variety of systems, basic parallel processes are rather limited. The main results of the paper are that the model checking problem is decidable for an expressive linear time logic (the linear time mu-calculus) and Petri nets, but undecidable for a weak branching time logic (a fragment of UB) and basic parallel processes.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$2365701D-F496-4DE0-8FC7-31F2B0717482","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920224$684099CB-FE1E-4D1D-891C-108A695B5B8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920224$302156B7-540B-462C-814F-8D4C67A3C8DF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4e586151820b2c8a12c5d8a7d2575c35c7a6e660","datavalue":{"value":"918709","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920224$ADD95117-23D3-45AA-97A4-90DAAA57273F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b43e972181ce91ebeb6a60807e78fc3d40d0a68e","datavalue":{"value":"linear logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$4057CC77-F50D-4B4C-B3F4-4CA651D53436","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb9f8004d477a3922fe8bde53d670f8b57c48852","datavalue":{"value":"model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$21779E73-D449-427C-B586-B7B18A82EB40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3a326f4d769b4e93379d3f0b8020f05faa527d36","datavalue":{"value":"branching logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$913F94E9-6E8B-445B-98A5-E6FA0F27106D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"981b12f1c489ffcbc71eecb28b735888668e0864","datavalue":{"value":"concurrent computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$AAE0A770-F545-430D-8B5F-114559C6853B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01a2e30b6f10c98d548518426a25a350ad19ecc5","datavalue":{"value":"Petri nets","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$55F65E71-B2A1-4007-94AB-1BD19EE53A58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6624cd6aa809cbeb3aea8d8a5c262cf35436bf48","datavalue":{"value":"parallel processes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$A4554FA8-480A-4B22-96DF-F8293081412A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7aa3fdbdf3b7584bcd007098b5e184978502a1cf","datavalue":{"value":"mu-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1920224$E1EA65EE-8CE0-48DF-AC62-A66D37F4A258","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":"Q1920224$08B2C22E-3A19-43E1-962D-C85108C517FA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0ec4a45c1f08374349794ed8398538c8be9d80c9","datavalue":{"value":"https://doi.org/10.1007/s002360050074","type":"string"},"datatype":"url"},"type":"statement","id":"Q1920224$C322D14E-7CC2-48BE-BBDB-CD26517FCE2D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6bdd414e9cb087d1bd0fee0f76cf914c94791585","datavalue":{"value":"W1977601940","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920224$8D80A559-038F-46EA-A26E-65BA2F498CE3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f215711294b586eb8d79bd94ab54c33ebe78d84e","datavalue":{"value":"10.1007/S002360050074","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1920224$C63F7B2C-1086-4688-A255-697928959BD4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3c453744c49ca3054b0709c44051fe1b80bcdc4","datavalue":{"value":{"entity-type":"item","numeric-id":4234763,"id":"Q4234763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96237116eb3d664c9e3f6a0e9ba1da888570c670","datavalue":{"value":{"amount":"+0.8632262349128723","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":"Q1920224$2D6F1809-0E26-4483-B190-80D79905A8AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a73a329faec39b433b6f8ba51390cf9198a041b7","datavalue":{"value":{"entity-type":"item","numeric-id":4289279,"id":"Q4289279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96237116eb3d664c9e3f6a0e9ba1da888570c670","datavalue":{"value":{"amount":"+0.8632262349128723","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":"Q1920224$AFB73888-B97C-4DFC-BBCC-6750264FF751","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72abbf54b2ae59348e2fd7ee081ec2416c538ec3","datavalue":{"value":{"entity-type":"item","numeric-id":4954445,"id":"Q4954445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"965c1c514a8eb9d780830c21e75e07f095e26d6e","datavalue":{"value":{"amount":"+0.8580971956253052","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":"Q1920224$5315473D-A771-4358-B239-3BA7DF14963A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6effe004b11319500cf470d640839e2d3ae7e058","datavalue":{"value":{"entity-type":"item","numeric-id":438572,"id":"Q438572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ae72be182cbba13751ecdd14fabb9114174523e","datavalue":{"value":{"amount":"+0.8303350210189819","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":"Q1920224$4E44C667-3B95-41BE-89B6-08C1360391C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3bd811b5d4f82a6fae6c59b30398f7c1bad898ee","datavalue":{"value":{"entity-type":"item","numeric-id":5699482,"id":"Q5699482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f69261bca3da8305e13ae5a9ef3da92a4082500","datavalue":{"value":{"amount":"+0.8254185318946838","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":"Q1920224$87F1C7CD-4844-4D74-B654-E7EA94FDF7B2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1920224","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1920224"}}}}}