• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Book chapter
  • On the model checking of sequential reactive systems
  • RU
  • EN
Расширенный поиск
Высшая школа экономики
Национальный исследовательский университет
Priority areas
  • business informatics
  • economics
  • engineering science
  • humanitarian
  • IT and mathematics
  • law
  • management
  • mathematics
  • sociology
  • state and public administration
by year
  • 2028
  • 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
September 18, 2026
When Pictures Hinder Understanding: Illustrations May Impede Learning of Abstract Ideas
Illustrations can help remember specific actions but do not always make abstract ideas easier to learn. Researchers from HSE University and Humboldt University compared how people learn from texts with different levels of abstractness. They found that participants remembered illustrations better and performed better on related tasks after reading a multimedia text about yoga asanas than after reading an abstract text about the Nash equilibrium. The findings could help improve the selection of illustrations for educational and informational materials. The study has been published in Learning and Instruction.
September 17, 2026
'I Wish That People Would Place Greater Trust in Science'
When Tatiana Eremicheva chose Fundamental and Computational Linguistics as her field of study, she thought it would be about learning languages. Instead, she discovered it was about helping people. In this interview for the HSE Young Scientists project, she discusses science as a way of understanding the world, billiards as a team-building activity, and why learning to read is not always as easy as it seems.
September 15, 2026
Immunity to Chaos: How Personal Resources Help Us Cope with the Challenges of a Turbulent World
International conflicts, crises and digital overload—the modern world puts our minds to the test every day. Traditional psychology often focuses on the consequences: anxiety, depression, and psychosomatic disorders. But what if we looked at the problem differently—through the lens of the resources that prevent us from breaking down? Psychological immunity is precisely this set of resources. Alena Zolotareva and her group, Psychological Immunity as a Resource for Positive Functioning, are developing an integrative model of this phenomenon, adapting diagnostic tools and preparing for large-scale empirical research. Why do psychologists need to collaborate with medical professionals, and how could their research transform preventive care in clinics and corporations?

 

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 the model checking of sequential reactive systems

P. 233–244.
Zakharov V., Kozlova D.

By sequential reactive system we mean a program which operates in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data a program performs a sequence of actions (response) and displays the current result. Such programs usually arise at implementation of computer drivers, online algorithms, control procedures. Basic actions performed by these programs may be regarded as generating elements of a certain semigroup. This consideration opens the way to model sequential reactive systems by finite state transducers that operate over semigroups. This model of computation is suitable for synthesis, optimization, verification and testing of sequential reactive systems. In this paper we originate a framework for developing verification techniques for sequential reactive systems by utilizing finite state transducers as a formal model. To this end we introduce a LTL-based formal language which may be suitable for specification of the behaviour of sequential reactive systems and adopt a well known LTL-based model checking techniques for verification of finite state transducers against these specifications.
 

Language: English
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

Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016.
Vol. 1698. , Humboldt-Universität zu Berlin, 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