{"entities":{"Q974119":{"pageid":975967,"ns":120,"title":"Item:Q974119","lastrevid":65909820,"modified":"2026-04-12T06:11:52Z","type":"item","id":"Q974119","labels":{"en":{"language":"en","value":"Complexity of metric temporal logics with counting and the Pnueli modalities"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5712829"}},"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":"Q974119$40A344A6-F654-46E4-B8AC-F3D5481A1B00","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"92176512ce20d4b9ef6eca4fc4cf558cd6c40657","datavalue":{"value":{"text":"Complexity of metric temporal logics with counting and the Pnueli modalities","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q974119$8E65BFB8-28C8-4A9D-A52B-ACDCEB1805C9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"98b3c2c7be4481c5e513744245ebe271ef3dfe75","datavalue":{"value":"1196.03029","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q974119$65708E07-9070-4B05-82B5-941C46F8D48B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"91a6d5b55b11b7c5072badc33d9b23eaf1c7a459","datavalue":{"value":{"entity-type":"item","numeric-id":259067,"id":"Q259067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$06C1C760-57F0-4515-A8A2-FC2E19BB1A30","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$281BCF2F-B101-43A0-A420-15E99E2B1308","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e2fe2a9116b611a4e0cd03f6e91b5254a2aef5ed","datavalue":{"value":{"time":"+2010-05-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q974119$33D6F430-98E3-4070-A8D6-6D460589E4EC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"28233eaeeb129eeed9583049fbf493b51d5accf4","datavalue":{"value":"This paper further develops the theory of metric temporal logics over continuous time. More specifically, the paper studies the complexity of the satisfiability problem for the logics TLC and TLP.   Here, TLC is the temporal logic with Until and Since operators extended with counting modalities \\(C_k(X)\\) that express that ``\\(X\\) is true at least \\(k\\) times in the unit interval ahead''. TLP is the temporal logic with Until and Since operators extended with the so-called Pnueli modalities \\(\\mathrm{Pn}_k(X_1,\\dots,X_k)\\) that express that there is an increasing sequence of points \\(t_1,\\dots,t_k\\) in the unit interval ahead such that \\(X_i\\) is true at \\(t_i\\).   The logics TLC and TLP have been introduced and studied in earlier work by \\textit{Y. Hirshfeld} and \\textit{A. Rabinovich} [Lect. Notes Comput. Sci. 1644, 422--432 (1999; Zbl 0939.03023); Log. Methods Comput. Sci. 3, No.~1, Paper 3, 11~p. (2007; Zbl 1128.03007)], where it was shown that TLC and TLP have the same expressive power and are both decidable. The main results of this paper are the exact complexity bounds for the satisfiability problem of TLC and TLP. The satisfiability problem for TLP is PSPACE-complete. The satisfiability problem for TLC is PSPACE-complete if one uses unary coding for the indices of the operators \\(C_k\\), and it is EXPSPACE-complete if one uses binary coding for these indices.","type":"string"},"datatype":"string"},"type":"statement","id":"Q974119$36E52E88-DCC7-4B28-88EE-0EA2EE8252CB","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"20ea4d830b8858745f047ee58c909a25f2934f0a","datavalue":{"value":{"entity-type":"item","numeric-id":618168,"id":"Q618168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$86BECB50-D4B9-4063-A99E-E36B83AAA551","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q974119$F4667F50-8A3C-4CB3-A3A4-7E93A4FDFC86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q974119$FCA39C6B-AFC9-47A7-8B8C-481BEC873529","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7845c751e73f158262f52fe1189862119b58a5fe","datavalue":{"value":"5712829","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q974119$719B6EEE-447D-4AD8-889B-F51E722FA9C0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q974119$B03205CD-D2ED-4A0C-A578-3D27F6494122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f8382ba04f9f05f645b4d0e4b9ea28f0619583","datavalue":{"value":"complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q974119$7BF4AC50-45F5-4E3A-A441-2B9B7C6A057B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e16fdb519452f3bafdb17bd5ad06b8194f047110","datavalue":{"value":"expressive power","type":"string"},"datatype":"string"},"type":"statement","id":"Q974119$300CDF96-4FC3-4677-A840-20DBDA9026AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bfded98921fb7d9cf722f229333546d869ef30c7","datavalue":{"value":"satisfiability problems","type":"string"},"datatype":"string"},"type":"statement","id":"Q974119$59B209C5-5653-490C-A4F4-E9254336B810","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":"Q974119$7D16BEFC-08BE-477F-BA64-3E348EBDEBF5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"46e9f77fdb529a9fbd4133e3289d4aab822e603f","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2010.03.017","type":"string"},"datatype":"url"},"type":"statement","id":"Q974119$78F2D16D-629B-4E16-8DC1-261DD7F10148","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4124ce8be90ee0600b09dd80c4a85aca737e0bfa","datavalue":{"value":"W2043086238","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q974119$305528E1-DD72-4AFA-81E7-6C6B4D78EB3E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8e019e14c862ddaf7bcd66cd64d6515bc5dc195","datavalue":{"value":{"entity-type":"item","numeric-id":4371517,"id":"Q4371517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$B4D7E04A-67EC-42D7-8827-41126ACD4947","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9f21257d8b20ccfecd3db595afbc8b2e1a0a737","datavalue":{"value":{"entity-type":"item","numeric-id":3835817,"id":"Q3835817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$88037C3A-3EE5-4F63-BEA5-38CA86813087","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bd2e069871eb3bf4232917297a8392cabd79fa8","datavalue":{"value":{"entity-type":"item","numeric-id":4251919,"id":"Q4251919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$948EDCE9-AA5A-4644-BFCF-B4BF821B8B65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f20e74feaba62bd46513e7af48c16a7db530206d","datavalue":{"value":{"entity-type":"item","numeric-id":4938638,"id":"Q4938638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$CF137EE2-7881-42A9-B60B-34F14515E465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da4bb6f9cf8d59bb08e30fa860898c4d527ef942","datavalue":{"value":{"entity-type":"item","numeric-id":4945224,"id":"Q4945224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$D4DD72AC-307B-4D1B-A8CA-D373E6B4546A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e828e5e129d51b8575c30bc55db9c76d50bd294","datavalue":{"value":{"entity-type":"item","numeric-id":4824483,"id":"Q4824483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$1E78DC0D-7A67-4A77-8FD1-D3C469F5C901","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b286d85c0ec526c88453b961ee0940519b5e9a61","datavalue":{"value":{"entity-type":"item","numeric-id":1780454,"id":"Q1780454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$9DFCC10B-A9E7-41DD-A1B3-55387BE65CF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"272609bd8b38f994632dd41505735fd6ac673cfb","datavalue":{"value":{"entity-type":"item","numeric-id":5756667,"id":"Q5756667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$5AACD410-D9F2-46DC-A2F8-9BDDEAD6328B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfa47655d911cd54ec5a24c13fe6c4246d8dad9a","datavalue":{"value":{"entity-type":"item","numeric-id":5310679,"id":"Q5310679"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$722DC233-7380-46EC-A384-60C22AD69A25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5781430c3bcca2b0df40d4fc7fd2bfdf2c1936f2","datavalue":{"value":{"entity-type":"item","numeric-id":1323323,"id":"Q1323323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$8CCEEA1E-876B-4E50-8014-3DEF8AC394D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab8bd75bf9da31e4849e1d172ea84f0ff8d354dd","datavalue":{"value":{"entity-type":"item","numeric-id":868030,"id":"Q868030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$1C8F6F1A-4B6C-4334-8C1D-C469F700DD06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b05b18de27616ff2350cf767a17b5adca2f692b4","datavalue":{"value":{"entity-type":"item","numeric-id":3543292,"id":"Q3543292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q974119$13DD660B-E39B-4A68-B8D1-12CEFFDC0AC0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"af14b90ce12036e6ac916443261959938abe1ea5","datavalue":{"value":"10.1016/J.TCS.2010.03.017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q974119$CB76AC06-2141-404A-95CD-AA5A4B5C1D21","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e5d21bc5f5fddcb5d589bce6c36f0cb306f10470","datavalue":{"value":{"entity-type":"item","numeric-id":3543292,"id":"Q3543292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f1f5e0fc624be0ea770c6e902cdd41774224d3d","datavalue":{"value":{"amount":"+0.89501816","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":"Q974119$E7D55FE8-745E-4DB5-8803-DC5A81A3D7CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"35cd83ccafccc2fbcd705a8d6d446c4166c2f692","datavalue":{"value":{"entity-type":"item","numeric-id":418179,"id":"Q418179"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72a563c371793c22314278f4a9f7ba4ae16cb9c7","datavalue":{"value":{"amount":"+0.83856165","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":"Q974119$C175EE3D-9336-4360-81BC-F67B1F777E2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"08187fb0101952b9f4dad3c72d2e27f324612e0b","datavalue":{"value":{"entity-type":"item","numeric-id":3511245,"id":"Q3511245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33b554d8ba6da5f76a29b537f25bb1426bee4a52","datavalue":{"value":{"amount":"+0.8331096","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":"Q974119$908D45E1-F753-4E14-9F2F-DB3E1EE95CC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be1aed6e5c14c75c02baea5233978724af3c3a31","datavalue":{"value":{"entity-type":"item","numeric-id":868030,"id":"Q868030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c64f52bde5af150ec8bd9a268a2ea33a5c9ac331","datavalue":{"value":{"amount":"+0.8172078","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":"Q974119$142B66A4-7079-4221-B9CB-DE09C8777D70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"03ad0d77aa2ff75e4f234583be0d095382d6df8b","datavalue":{"value":{"entity-type":"item","numeric-id":3184695,"id":"Q3184695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e035577da3b2b455112f2099c7bb4f263800002","datavalue":{"value":{"amount":"+0.81309056","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":"Q974119$3AE2142E-03D2-4B50-A326-6C861C969CF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"472e2390860ce0843a5faf10aa4ef23ded5b0577","datavalue":{"value":{"entity-type":"item","numeric-id":999264,"id":"Q999264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6975cc158a6535fcd994c0516dfd3628e5b5134","datavalue":{"value":{"amount":"+0.81088847","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":"Q974119$98870B73-0FFF-4910-861F-560606DD7EB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3ab9f2509c21cca89f4ce19e2769db4489bec08f","datavalue":{"value":{"entity-type":"item","numeric-id":2228435,"id":"Q2228435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06e9f5bd0210e070c8c3eda107517f1a975f8c37","datavalue":{"value":{"amount":"+0.8080086","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":"Q974119$DB4B6AC9-A0A0-4F5A-BDE0-AFBDD43E432E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ba14abcaf83459f7ae606f3426b2335e3bd0598","datavalue":{"value":{"entity-type":"item","numeric-id":2811351,"id":"Q2811351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56c3af52ef0725ea4f126e91ddd582fb2b156248","datavalue":{"value":{"amount":"+0.8068328","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":"Q974119$945748EF-2BD5-45E6-8E57-4B51E605755D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a08b9742aed72fccf004aa83edda5ac5afff1dc7","datavalue":{"value":{"entity-type":"item","numeric-id":5899090,"id":"Q5899090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10b2146ad0326959ad4b50381e62e5a195e4fbe1","datavalue":{"value":{"amount":"+0.8065107","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":"Q974119$CD77304B-408C-4DC1-BE22-05115AB9EA22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dea6cef1071023ec3c7c09641c7c2f0dd9d30998","datavalue":{"value":{"entity-type":"item","numeric-id":3296347,"id":"Q3296347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be6cf6327537a00ca9f1ae3a4d4f25ae4fdd5f31","datavalue":{"value":{"amount":"+0.8058894","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":"Q974119$F2B75C19-60D3-400E-BDBC-81DCB6CEA44E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Complexity of metric temporal logics with counting and the Pnueli modalities","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Complexity_of_metric_temporal_logics_with_counting_and_the_Pnueli_modalities"}}}}}