{"entities":{"Q1917070":{"pageid":1927812,"ns":120,"title":"Item:Q1917070","lastrevid":43420573,"modified":"2025-07-25T16:23:56Z","type":"item","id":"Q1917070","labels":{"en":{"language":"en","value":"A temporal logic for proving properties of topologically general executions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 896627"}},"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":"Q1917070$CB5DDE3E-2AEA-46AB-B160-4A0C854920D2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"df7b184d334b39553cd4362afd410cb42ee93967","datavalue":{"value":{"text":"A temporal logic for proving properties of topologically general executions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1917070$E213420B-6334-4A4C-9123-30250981E4CD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"17f251eb70c860c1620c97c124bdf8596ef3c428","datavalue":{"value":"0861.03024","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$ED766CF0-56D3-421B-9178-414D74116607","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1ebc16da0076a87e7f942c6c122af0f909000e36","datavalue":{"value":{"entity-type":"item","numeric-id":1380413,"id":"Q1380413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1917070$BCCABA21-1154-469B-AAC8-E2A5D56163C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"16de316f302fba13aeaf995a5fa68cb2abb070f8","datavalue":{"value":{"entity-type":"item","numeric-id":225931,"id":"Q225931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1917070$697CD021-F915-4D34-86CD-F87616A0F0AF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1917070$96783F7A-04DA-47B7-8024-0ADF3441DE6D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e6c12cf0fa9e38f832c0f5cac78fe70e7e278753","datavalue":{"value":{"time":"+1997-05-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1917070$7CEA1A91-AF24-40FA-829B-4EB375C5B934","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"697f3dce130ca5ca0f6d470ce3bbe32b60d37a0e","datavalue":{"value":"When considering correctness and termination of (possibly infinite) computations of nondeterministic or parallel programs, usually one restricts the attention to particular kinds of computation (e.g., fair ones) with the implicit assumption that they represent the more ``generic'' case. \\textit{D. Lehmann} and \\textit{S. Shelah} [Inf. Control 53, 165-198 (1982; Zbl 0523.03016)] proposed a formal system based on temporal logics which allows one to prove properties of probabilistic programs, when these properties hold for ``most'' (in the probabilistic sense) computations. In this paper, the authors reinterpret such a formal system by considering a different semantics for it, which is based on the topological notion of ``co-meagre'' set of computation paths. This provides an adequate formalization of the concept of ``generic'' computation, since the ``meagre'' set is well known to topologists as an adequate formalization of the notion of ``exceptional'' or ``non-generic''. The authors prove that the system defined by Lehmann and Shelah is sound and complete for this topological interpretation, thus obtaining a system which can be used for reasoning about properties of ``generic'' computations of non-deterministic or parallel programs. Another interesting fact is that the system has the finite model property, namely every sentence having a model (in general a tree model of arbitrary size) has a finite model.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$B263CDD5-DB74-4946-9006-77F902115B60","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$D83B0374-4640-4254-A9C7-505F10B2F708","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$CF066262-C15C-4E41-9FDC-4FB73BB734AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$FC3578C0-A04C-42C5-AA6A-539F9EFCF759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"35bbdcbda53152c249a7f99650e19b5ef62999f2","datavalue":{"value":"68Q10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$4C72A287-9D58-4503-9954-CDA8B5B72EFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4388e9a976e18bebff2edd807ee73ae25eae8b00","datavalue":{"value":"54E52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$64152ADA-6220-4580-B3D6-FDC47F7DDF78","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6cf23b6b37cca4ceb9f1c643f890c8e0a32433ec","datavalue":{"value":"896627","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$56A8646A-304E-4500-83E8-F0495F8AD6B5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$01E6EDF3-1DF2-4C40-9B1E-C0C8AA54CE98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb4fb8c29fbb296345b09a1840f7931ec0647a4e","datavalue":{"value":"program properties","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$7053A1CE-A80E-4008-8911-E483F6D60327","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ab974973fe30cd79fb08fe157a1e54054f866a7","datavalue":{"value":"co-meagre sets","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$A4D873FB-F286-42B9-A960-11A207A90D54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"855af08d63de68a214880a14dc080a2a72230738","datavalue":{"value":"parallel programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$3B9B5183-5BF6-4997-885F-18069B9CA764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"abb803c6475a042fe06038cc89389e508b9ca513","datavalue":{"value":"probabilistic programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$6558F797-CC88-40F6-A45B-A22A445A7336","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"76d30cb4011454775662cabcfb0dee19104a75ca","datavalue":{"value":"topological interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$821C983B-CAC3-49BA-B352-AEE409B54D29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fc481c9956349136fb46ebae74b8442d2d25b871","datavalue":{"value":"finite model property","type":"string"},"datatype":"string"},"type":"statement","id":"Q1917070$2F0C22EB-CF5E-48C3-9D74-B6AD77F9D500","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"b9de049e0779ede1d4a5df8a04a7e663dace2f18","datavalue":{"value":{"entity-type":"item","numeric-id":276550,"id":"Q276550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1917070$1E3993B1-13A6-4CCE-A0FC-AD7E24329899","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":"Q1917070$5EA2E5A9-949B-4FB4-97FA-DE56C9B2AD80","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"66241c46de1ab5fe0ee29933fa8fcce9eefbe438","datavalue":{"value":"https://doi.org/10.1006/inco.1996.0010","type":"string"},"datatype":"url"},"type":"statement","id":"Q1917070$D0B5673C-7E45-411C-BD23-E49EFAC1444F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"df01d1c18daed1296cca30bf83659cf16a5e8fea","datavalue":{"value":"W2000847132","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$8D8F96A4-1271-4CEF-8505-BD85689453B4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4f490354aafd3bc21ce3a6248480d498a12da3e7","datavalue":{"value":"10.1006/INCO.1996.0010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1917070$A33A35F6-787B-46CE-A43A-48819BC726F9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"320b564d9f4f19744106617d05644e9d8840469a","datavalue":{"value":{"entity-type":"item","numeric-id":2956706,"id":"Q2956706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e447822cd9e34d6d0491cb9b0283332b7d114b59","datavalue":{"value":{"amount":"+0.7970907","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$FF843775-596F-436D-9F92-87BA530CAC60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0da88f1253fdb67fff95e2b857e74ac4fd8f9abd","datavalue":{"value":{"entity-type":"item","numeric-id":5325837,"id":"Q5325837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"829743fbf7edc95717b01a29eae9405e37f81329","datavalue":{"value":{"amount":"+0.78266746","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$0C32C296-27FC-403B-A57B-2328AC052A1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fc5bbcca317ee7c4797c4aa77033fb46e5480b43","datavalue":{"value":{"entity-type":"item","numeric-id":1803654,"id":"Q1803654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72ba70030565cddb6b203c37fff27567f7b71891","datavalue":{"value":{"amount":"+0.7793628","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$B06A3E93-EA92-4A48-A06D-722019DDA3B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"069e430bb430cd217bb003a396d40fed1851271a","datavalue":{"value":{"entity-type":"item","numeric-id":3021957,"id":"Q3021957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e18c758b39403124268bef07bd9714c96dd536b1","datavalue":{"value":{"amount":"+0.77584016","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$5489A8C1-1959-4CD0-B175-D53976319DB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0f857a912907ee72717c5b9c388e6fabe6e5085","datavalue":{"value":{"entity-type":"item","numeric-id":5009454,"id":"Q5009454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"291aa4cbcfda0134e7c26216307c8344494423f4","datavalue":{"value":{"amount":"+0.76999617","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$4AF97706-2D4C-45E1-B033-484E78109F60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"429f664986c3991914912f223791a9bf6c6c0370","datavalue":{"value":{"entity-type":"item","numeric-id":4650346,"id":"Q4650346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7cb8d439b30766b20edb28ad1fbae41aa6a3644c","datavalue":{"value":{"amount":"+0.76969403","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$E2685A55-0560-4561-B6FA-7E4D6759E0E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6145a40c5d2afbcd19d7b48b52bb00296d6f75b","datavalue":{"value":{"entity-type":"item","numeric-id":4722046,"id":"Q4722046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"661795f918034ddcf203179501f8040e3a7191bb","datavalue":{"value":{"amount":"+0.7678888","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$F0D4A06D-3EE7-41F9-B46A-5B517284DCD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81b216213f6a059cf7f0308148fcacfeaf4a13dd","datavalue":{"value":{"entity-type":"item","numeric-id":2802489,"id":"Q2802489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"62e84f2bfdafb0499258cfd122fb94ed3e99ca6c","datavalue":{"value":{"amount":"+0.7650405","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$8CB73C42-5235-44CB-9DE7-59085E1C7EF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ffd31365b997de4d19740c327b0da27c026f29ee","datavalue":{"value":{"entity-type":"item","numeric-id":1079944,"id":"Q1079944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"73974bc56a91858380b9d8808703bc882d086344","datavalue":{"value":{"amount":"+0.7643094","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$891BAE6C-9ABF-45A3-9B38-99D92B0ED4B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f374c4601b8a6b887bb705c7e3de04b330ea985a","datavalue":{"value":{"entity-type":"item","numeric-id":1112586,"id":"Q1112586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25b5282f4ef02a6213a32a7c04c5a6cd3af0c3bb","datavalue":{"value":{"amount":"+0.76398075","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1917070$5FCA1374-5CA8-4DC4-A910-93D5B3F0465B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1917070","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1917070"}}}}}