• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • Темпоральная логика для верификации автоматов-преобразователей
  • 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
June 3, 2026
Pocket Money, Personal Interest, and Family Practices: What Shapes Students Economic Literacy?
University students' economic literacy depends not only on their field of study but also on their interest in economics, the learning environment, and family financial practices. For example, students who received pocket money irregularly tend to perform better on economic literacy tests than their peers who received financial support on a regular basis. These findings come from a study conducted by HSE University involving more than 1,100 students from five Russian universities. The findings have been published in Cakrawala Pendidikan.
June 3, 2026
Creative Work as a Remedy for Burnout
The creative, supportive atmosphere and innovative methods at the Centre for Sociocultural Research make it appealing to early-career scholars. Over years of working at HSE University, they grow into researchers and lecturers recognised both in Russia and abroad. Chief Research Fellow Zarina Lepshokova and Leading Research Fellow Ekaterina Bushina spoke about their journey at the centre and at HSE, their research, and the role of mentors in their academic success.
June 2, 2026
HSE Study Reveals Imbalance in the Generative AI Market
Researchers at HSE University analysed how effectively the global generative artificial intelligence market converts investment into real revenue, concluding that AI is currently developing faster than it is paying off. The results have been published in the journal Foresight and STI Governance.

 

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

?

Темпоральная логика для верификации автоматов-преобразователей

С. 204–206.
Zakharov V., Козлова Д. Г.
Language: Russian
Text on another site
Keywords: model checkingfinite state transducerконечный автомат-преобразовательверификация моделей программтемпоральная логикаtemporal logic
Publication based on the results of:
Modeling and analysis of the behavior of distributed process-aware information systems (2016)

In book

Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.)
М.: Изд-во механико-математического факультета МГУ, 2016.
Similar publications
Merging Epistemic and Temporal Models: a History-Free Approach
Popova E., Логико-философские штудии 2022 Vol. 20 No. 1 P. 1–7
There are two approaches to merging temporal and epistemic models. The first one consists in starting with a temporal model and enriching it with epistemic dimension (as temporal epistemic logic), while the second one is supposed to start with an epistemic model introducing temporal dimension (dynamic epistemic logic, epistemic temporal logic). The proposed evolutionary epistemic ...
Added: August 1, 2022
On the Model Checking Problem for Some Extension of CTL*
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776–785
Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The results of operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often ...
Added: January 17, 2022
Efficient Equivalence Checking Technique for Some Classes of Finite-State Machines
Zakharov V., Automatic Control and Computer Sciences (AC&CS), Switzerland 2021 Vol. 55 No. 7 P. 670–701
Finite transducers, two-tape automata, and biautomata are related computational models descended from the concept of finite-state automaton. In these models an automaton controls two heads that read or write symbols on the tapes in the one-way mode. The computations of these three types of automata show many common features, and it is surprising that the methods for analyzing ...
Added: January 17, 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
Reasoning Web. Declarative Artificial Intelligence, 16th International Summer School 2020, Oslo, Norway, June 24-26, 2020, Tutorial Lectures. Article: Temporal Ontology-Mediated Queries and First-Order Rewritability: A Short Course
Zakharyaschev M., Ryzhikov V., Wałęga P., Springer Publishing Company, 2020.
Added: November 8, 2021
Branching Time Logics with Multiagent Temporal Accessibility Relations
Rybakov V., Siberian Mathematical Journal 2021 Vol. 62 P. 503–510
Under study are the branching time temporal logics with temporal accessibility relations for the agents different in length and content. We find an algorithm for solving the problems of satisfiability and decidability of the logic through describing finite satisfiable models of computable size (through the size of the input formulas). We remove the constraints on the ...
Added: November 8, 2021
Conference: 28th International Symposium on Temporal Representation and Reasoning, TIME 2021
Zakharyaschev M., Savateev Y., Ryzhikov V., Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021.
Our concern is the problem of determining the data complexity of answering an ontology-mediated query (OMQ) given in linear temporal logic LTL over (Z, <) and deciding whether it is rewritable to an FO(<)-query, possibly with extra predicates. First, we observe that, in line with the circuit complexity and FO-definability of regular languages, OMQ answering ...
Added: November 6, 2021
Knowledge and Time: Evolutionary Epistemic Model
Popova E., , in: Двенадцатые Смирновские чтения: материалы Международной научной конференции, Москва, 24–26 июня 2021 г.: М.: Русское общество истории и философии науки, 2021. P. 134–137.
This paper is concerned with the formalization problem of a wide range of scenarios of how knowledge evolves over time. We focus on combinations of temporal and epistemic modalities reflecting various properties of rational agents’ deliberation. For this purpose, we introduce the model EEM – evolutionary epistemic model. ...
Added: June 28, 2021
О задаче верификации моделей программ для одного расширения логики CTL*
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 428–441
Sequential reactive systems include programs and devices that work with two streams of data and convert input streams ofdata into output streams. Such information processing systems include controllers, device drivers, computer interpreters.‘e result of the operation of such computing systems are in€nite sequences of pairs of events of the request–responsetype, and, therefore, €nite transducers are ...
Added: January 31, 2021
  • 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