• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • On complexity of propositional linear-time temporal logic with finitely many variables
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2027
  • 2026
  • 2025
  • 2024
  • 2023
  • 2022
  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012
  • 2011
  • 2010
  • 2009
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
  • 1999
  • 1998
  • 1997
  • 1996
  • 1995
  • 1994
  • 1993
  • 1992
  • 1991
  • 1990
  • 1989
  • 1988
  • 1987
  • 1986
  • 1985
  • 1984
  • 1983
  • 1982
  • 1981
  • 1980
  • 1979
  • 1978
  • 1977
  • 1976
  • 1975
  • 1974
  • 1973
  • 1972
  • 1971
  • 1970
  • 1969
  • 1968
  • 1967
  • 1966
  • 1965
  • 1964
  • 1963
  • 1958
  • More
Subject
News
April 28, 2026
Scientists Develop Algorithm for Accurate Financial Time Series Forecasting
Researchers at the HSE Faculty of Computer Science benchmarked more than 200,000 model configurations for predicting financial asset prices and realised volatility, showing that performance can be improved by filtering out noise at specific frequencies in advance. This technique increased accuracy in 65% of cases. The authors also developed their own algorithm, which achieves accuracy comparable to that of the best models while requiring less computational power. The study has been published in Applied Soft Computing.
April 27, 2026
Fair Division: How Mathematics Helps to Divide the Indivisible
How can items be allocated among participants so that no one feels short-changed? Alexander Karpov, Assistant Professor at the Faculty of Economic Sciences, and his Singaporean colleague, Prof. Warut Suksompong, set out to find a mathematical answer to this question. In this interview, they discuss how a model of rational preferences is constructed, why one cannot rely on a simple sum of values, and where an algorithm that asks a minimal number of questions can be useful.
April 24, 2026
Electronics of the Future: Why Superconductors and Spintronics Work Together
It was once believed that superconductivity and magnetism avoided each other like the devil avoids holy water. However, modern nanostructures prove the opposite. A Russian theoretical physicist and Indian experimentalists have joined forces to create the electronics of the future—free from energy losses. Nataliya Pugach, Professor at the School of Electronic Engineering at HSE MIEM and Leading Research Fellow at the Quantum Nanoelectronics Laboratory, explains how a long-standing acquaintance in Cambridge grew into a mirror laboratory project with the Indian Institute of Technology Bombay (IIT Bombay), how superconducting spintronics works, and what surprises a researcher in India beyond the university campus.

 

Have you spotted a typo?
Highlight it, click Ctrl+Enter and send us a message. Thank you for your help!

Publications
  • Books
  • Articles
  • Chapters of books
  • Working papers
  • Report a publication
  • Research at HSE

?

On complexity of propositional linear-time temporal logic with finitely many variables

P. 313–316.
Rybakov M., Shkatov D.

It is known that both satisfiability and model-checking problems for propositional Linear-time Temporal Logic, LTL, with only a single propositional variable in the language are PSPACE-complete, which coincides with the complexity of these problems for LTL with an arbitrary number of propositional variables. In the present paper, we show that the same result can be obtained by modifying the original proof of PSPACE-hardness for LTL; i.e., we show how to modify the construction to model the computations of polynomially-space bound Turing machines using only formulas of one variable. We believe that our alternative proof gives additional insight into the semantic and computational properties of LTL.

Language: English
DOI
Text on another site
Keywords: finite-variable fragmentsSatisfiability problemLinear-time Temporal Logicmodel-checking

In book

Proceedings of the Annual Conference of the South African Institute of Computer Scientists and Information Technologists
NY: ACM, 2018.
Similar publications
Complexity of finite-variable fragments of propositional temporal and modal logics of computation
Rybakov M., Shkatov D., Theoretical Computer Science 2022 Vol. 925 P. 45–60
We prove that branching-time temporal logics CTL and CTL* are polynomial-time embeddable into their single-variable fragments. It follows that satisfiability for CTL and CTL*, and therefore also for alternating-time temporal logics ATL and ATL*, in languages with one propositional variable is as algorithmically hard as satisfiability for the full logic: EXPTIME-complete for CTL and ATL, and 2EXPTIME-complete for CTL* and ATL*. We discuss applicability of the technique used in the proofs to other ...
Added: May 12, 2022
О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356–371
Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification ...
Added: January 17, 2022
First-order rewritability of ontology-mediated queries in linear temporal logic
Artale A., Kontchakov R., Kovtunova A. et al., Artificial Intelligence 2021 Vol. 299 Article 103536
We investigate ontology-based data access to temporal data. We consider temporal ontologies given in linear temporal logic LTL interpreted over discrete time . Queries are given in LTL or , monadic first-order logic with a built-in linear order. Our concern is first-order rewritability of ontology-mediated queries (OMQs) consisting of a temporal ontology and a query. By taking account of the temporal operators ...
Added: September 30, 2021
Undecidability of the logic of partial quasiary predicates
Rybakov M., Shkatov D., Logic Journal of the IGPL 2022 Vol. 30 No. 3 P. 519–533
We obtain an effective embedding of the classical predicate logic into the logic of partial quasiary predicates. The embedding has the property that an image of a non-theorem of the classical logic is refutable in a model of the logic of partial quasiary predicates that has the same cardinality as the classical countermodel of the ...
Added: May 29, 2021
Complexity of finite-variable fragments of products with K
Rybakov M., Shkatov D., Journal of Logic and Computation 2021 Vol. 31 No. 2 P. 426–443
It is shown that products and expanding relativized products of propositional modal logics where one component is the minimal monomodal logic K are polynomial-time reducible to their single-variable fragments. Therefore, the nown lower bound complexity and undecidability results for such logics are extended to their single-variable fragments. Similar results are obtained for products where one component is a polymodal logic with a K-style ...
Added: September 24, 2020
Algorithmic properties of first-order modal logics of the natural number line in restricted languages
Rybakov M., Shkatov D., , in: Advances in Modal LogicVol. 13.: College Publications, 2020. P. 523–539.
We study algorithmic properties of first-order predicate monomodal logics of the natural number line in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. The languages we consider have no constants, function symbols, or the equality symbol. We show that satisfiability for the logics of is not arithmitical in languages ...
Added: August 27, 2020
Complexity and expressivity of Branching- and Alternating-time temporal logics with finitely many variables
Rybakov M., Shkatov D., , in: Theoretical Aspects of Computing – ICTAC 2018Vol. 11187.: Springer, 2018. P. 396–414.
We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and ATL*, are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e., with an unlimited supply of propositional variables. It follows that satisfiability for CTL, as well as for ATL, with a single variable is EXPTIME-complete, ...
Added: October 8, 2019
Algorithmic properties of modal logics with restricted languages
Rybakov M., University of the Witwatersrand, Johannesburg, 2019.
Modal logics, both propositional and predicate, have been used in computer science since the late 1970s. One of the most important properties of modal logics of relevance to their applications in computer science is the complexity of their satisfiability problem. The complexity of satisfiability for modal logics is rather high: it ranges from NP-complete to ...
Added: October 5, 2019
  • About
  • About
  • Key Figures & Facts
  • Sustainability at HSE University
  • Faculties & Departments
  • International Partnerships
  • Faculty & Staff
  • HSE Buildings
  • HSE University for Persons with Disabilities
  • Public Enquiries
  • Studies
  • Admissions
  • Programme Catalogue
  • Undergraduate
  • Graduate
  • Exchange Programmes
  • Summer University
  • Summer Schools
  • Semester in Moscow
  • Business Internship
  • Research
  • International Laboratories
  • Research Centres
  • Research Projects
  • Monitoring Studies
  • Conferences & Seminars
  • Academic Jobs
  • Yasin (April) International Academic Conference on Economic and Social Development
  • Media & Resources
  • Publications by staff
  • HSE Journals
  • Publishing House
  • iq.hse.ru: commentary by HSE experts
  • Library
  • Economic & Social Data Archive
  • Video
  • HSE Repository of Socio-Economic Information
  • HSE1993–2026
  • Contacts
  • Copyright
  • Privacy Policy
  • Site Map
Edit