{"entities":{"Q800722":{"pageid":802570,"ns":120,"title":"Item:Q800722","lastrevid":64469088,"modified":"2026-04-11T20:04:50Z","type":"item","id":"Q800722","labels":{"en":{"language":"en","value":"A generalized nexttime operator in temporal logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3878350"}},"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":"Q800722$C0D6C833-C69C-4874-9949-2A20ACEEF400","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"407ee0b40fe2e9d8970a1f84db10774d127dfce5","datavalue":{"value":{"text":"A generalized nexttime operator in temporal logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q800722$12F605FC-C499-4341-A324-5B80F5083DDE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"146d018f0a44fd3669de2ab0b4da12a8cce9ea59","datavalue":{"value":"0551.68032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800722$1F1CBAE2-2E0D-40B3-A8E1-D8EDCFEB7945","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d7fb3df4b18cf56b1220f5118b2e44e5f7f04a82","datavalue":{"value":"10.1016/0022-0000(84)90015-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800722$EF709201-511D-45A7-B9D8-7922C0597E60","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c5832f8876614de1887b6fff71a1066143db327e","datavalue":{"value":{"entity-type":"item","numeric-id":786129,"id":"Q786129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$9961787A-E4A2-48A1-A405-CE7259F0E51B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3340243f57e05f2265c56423c388055a14b114fa","datavalue":{"value":{"entity-type":"item","numeric-id":107189,"id":"Q107189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$D4EAB375-EB0B-4EAD-87A3-7B5A15742138","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q800722$F5A87347-BB69-4157-AC05-33D607C8C57F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"026cef6f636a0508366bd75af6d53948bb1bc46f","datavalue":{"value":"The paper introduces a new binary operator ''atnext'' into temporal logic generalizing the usual nexttime operator in a straightforward way. Some dualities with the until operator are proved which also show that the new operator has the same expressive power as ''until''. An axiomatization and several proof rules are given. An example (the alternating bit protocol) shows how the operator can profitably be used to describe and prove safety properties of programs.","type":"string"},"datatype":"string"},"type":"statement","id":"Q800722$2763401B-5E04-4DC4-810F-D88097BFA040","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800722$30B3CD7B-9A77-488F-8C1D-0E56F72F6BFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800722$2B02EA05-56BC-49EC-9D7C-CC19817FC86E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800722$B0554B69-FC49-42D5-8B12-B6EBBC80ED97","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8f9fb10cf102f6eb59988e9353d01523c10655ba","datavalue":{"value":"3878350","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800722$E2D69538-A29C-452B-A525-277DB96DD41C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q800722$BE4AB82C-816F-448F-A9F6-D8FD1A44EB1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75a311538226cc5f4628ef610729f113a981264d","datavalue":{"value":"nexttime operator","type":"string"},"datatype":"string"},"type":"statement","id":"Q800722$80CB9473-32B6-4E6E-93D5-F78370D38368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d1faca1adebeea373ff57547e505d2e89b3af7e8","datavalue":{"value":"until operator","type":"string"},"datatype":"string"},"type":"statement","id":"Q800722$FC55E793-D890-4C06-9990-0FFC9A2EAB98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06dacf54f2b6d6a113f47a7b4aee1e9d715afb58","datavalue":{"value":"alternating bit protocol","type":"string"},"datatype":"string"},"type":"statement","id":"Q800722$5DD52889-9F8B-4C3C-963B-B86064CB8BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a820724f1e5b1707259dc0c137d5986b8eec574a","datavalue":{"value":"safety properties of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q800722$B26AB138-4093-43CC-AADE-1AA68C436D80","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":"Q800722$2781B6AE-6A78-4478-9957-962EAD65A582","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"07e761a470af8614fd4248d16c2012bfb6e2bf30","datavalue":{"value":"https://doi.org/10.1016/0022-0000(84)90015-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q800722$619B93A7-4564-4FA1-9A73-BCCC119FB07F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ba7efb8217ea7fa7eac7ea55c32d4a82b4e94a3e","datavalue":{"value":"W2005856245","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q800722$51435A96-6CDD-4CAE-9391-C8ECE8033353","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ce646df2ba4e62a5e63c3ad929d766750f3eb86","datavalue":{"value":{"entity-type":"item","numeric-id":1159976,"id":"Q1159976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$7BFF179B-AE30-443C-93A8-5354400F2FC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085c05aaa57ddfc3bb4a6f1a1d4544fab76f2fb6","datavalue":{"value":{"entity-type":"item","numeric-id":4136521,"id":"Q4136521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$9DA47F8F-A3A5-409C-A47F-AA15AEA1B75D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9deaf5805369ed94d2c2b3ba23b0118b7817813","datavalue":{"value":{"entity-type":"item","numeric-id":4151145,"id":"Q4151145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$EE28F287-5BB5-4CFD-8F87-0E6D1A827C2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b824b740eea2d4e4e90cc1d7e35b816050e5929e","datavalue":{"value":{"entity-type":"item","numeric-id":1138900,"id":"Q1138900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$95F08BF8-517D-4410-BBB4-33C0CDF34A4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df755177511a4a382e9fd897da9fe34d7e867ddc","datavalue":{"value":{"entity-type":"item","numeric-id":5679697,"id":"Q5679697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$E7940274-3E2A-4E43-B85D-C08BDEC268F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68d7877f5c06b692012bb89ac63c690d31fa44f3","datavalue":{"value":{"entity-type":"item","numeric-id":3942371,"id":"Q3942371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$0EFC3AF5-4FC1-471D-900E-200737CCBE6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5410069e8abd75acf0c4dc99bb1a84758ddd17bf","datavalue":{"value":{"entity-type":"item","numeric-id":4187287,"id":"Q4187287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$211C6175-6340-4A85-9E72-3001486BDA87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8e3d5efcad955e9874c3cad0d3e003718384f33","datavalue":{"value":{"entity-type":"item","numeric-id":1143164,"id":"Q1143164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q800722$A3E89EED-7792-43AE-A9B8-D56F8A4B9390","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f12f09a85a3e80166149c364db6599477a28da1a","datavalue":{"value":{"entity-type":"item","numeric-id":3677141,"id":"Q3677141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed513e4dfe05c68fc4fb02ba120ebe3571868e75","datavalue":{"value":{"amount":"+0.8318812251091003","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":"Q800722$134B3E67-64DE-4455-B7C9-E64CB66AD49E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"309f995ebfc814203ab1311d6199f66c932e719f","datavalue":{"value":{"entity-type":"item","numeric-id":789895,"id":"Q789895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"752a28f23d5fd69392339c57b10a4e994736413f","datavalue":{"value":{"amount":"+0.7969716191291809","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":"Q800722$93E0DD64-F071-45BD-8D2F-7108C6FCF769","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"592765424e6503741bb123017c96976915414633","datavalue":{"value":{"entity-type":"item","numeric-id":3812208,"id":"Q3812208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd0343990602a669ee023f3247f7ec687e414eb6","datavalue":{"value":{"amount":"+0.7926543354988098","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":"Q800722$D21CF8C0-4432-4749-86B6-DED9224790E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76b347872709d7e70c765b6daeac5a422da11371","datavalue":{"value":{"entity-type":"item","numeric-id":3221966,"id":"Q3221966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"000aab39f83987f6d8c0674fb52b5cf6b550a0ed","datavalue":{"value":{"amount":"+0.792280375957489","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":"Q800722$D4F53FE8-A32E-46EE-8C03-3630BC99F724","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65b1dbbc66aa68ee1476d765265be7a93c44a3ac","datavalue":{"value":{"entity-type":"item","numeric-id":3028984,"id":"Q3028984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9cab80c1a8e5fae991a4cce215cae1d6a91ff90b","datavalue":{"value":{"amount":"+0.7921391129493713","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":"Q800722$46092770-F08C-4133-B319-C13204372D06","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A generalized nexttime operator in temporal logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_generalized_nexttime_operator_in_temporal_logic"}}}}}