• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • A
  • A
  • A
  • A
  • A
Обычная версия сайта
  • RU
  • EN
  • HSE University
  • Publications
  • Articles
  • Tool for Behavioral Analysis of Well-Structured Transition Systems
  • 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
November 9, 2026
'Organ-on-a-Chip Technology Could Eliminate the Need for Animal Testing'
The Laboratory of Molecular Physiology at the HSE Faculty of Biology and Biotechnology investigates how molecular regulators known as microRNAs control gene expression and contribute to the development of diseases, including cancer, viral and inflammatory conditions, and pregnancy complications. At HSE University, researchers develop organ-on-a-chip models: miniature devices containing living cells that mimic the functions of human organs, such as the placenta and intestines. These models help researchers understand how diseases develop and how drugs affect them. HSE News Service spoke with Evgeny Knyazev, Head of the Laboratory.
November 9, 2026
Flattened Terrain Models Underestimate Vehicle-to-Vehicle Communication Outages
Researchers at HSE MIEM have shown that widely used simulators of vehicle-to-vehicle communication significantly overestimate its reliability because they assume flat terrain. When terrain features, bridges, and tunnels are taken into account, the outage rate on a mountain serpentine road rises from 21% to 30%, on an overpass from 20% to 33%, and in a tunnel from 0% to 80%. The results have been published in Future Transportation.
November 6, 2026
Study Reveals Why Experienced Readers Sometimes Make Mistakes in Comprehension
Researchers at the HSE Centre for Language and Brain examined how people comprehend sentences in which the grammatical structure conveys a meaning that conflicts with assumptions based on their life experience. In an experiment, participants were asked to read sentences describing two characters and then identify which character had performed the action. The results showed that people with greater reading experience performed better when a character's actions matched their expectations but were more likely to make mistakes when the actions contradicted those expectations. The paper has been published in the Quarterly Journal of Experimental Psychology. The study was supported by a grant from the Russian Science Foundation.

 

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

?

Tool for Behavioral Analysis of Well-Structured Transition Systems

Proceedings of the Institute for System Programming of the RAS. 2017. Vol. 29. No. 4. P. 175–190.
Dworzanski L. W., Михайлов В. Е.

Well-structured transition systems (WSTS) became a well-known tool in the study of concurrency systems for proving decidability of properties based on coverability and boundedness. Each year brings new formalisms proven to be WSTS systems. Despite the large body of theoretical work on the WSTS theory, there has been a notable gap of empirical research of well-structured transition systems. In this paper, the tool for behavioural analysis of such systems is presented. We suggest the extension of SETL language to describe WSTS systems (WSTSL). It makes the description of new formalisms very close to the formal definition. Therefore, it is easy to introduce and modify new formalisms as well as conduct analysis of the behavioural properties without much programming efforts. It is highly convenient when a new formalism is still under active development. Two most studied algorithms for analysis of well-structured transition systems behavior (backward reachability and the Finite Reachability Tree analyses) have been implemented; and, their performance was measured through the runs on such models as Petri Nets and Lossy Channel Systems. The developed tool can be useful for incorporating and testing analysis methods to formalisms that occur to be well-structuredness transition systems.

Research target: Computer Science
Priority areas: IT and mathematics
Language: English
Full text
DOI
Text on another site
Keywords: сети ПетриPetri netsформальные методы программной инженерииwell structured transition systemsвполне структурированные системы переходовformal verificationinfinite state systemsсистемы с бесконечным числом состояний
Publication based on the results of:
Synthesis and analysis of process models (2017)
Similar publications
Machine Learning and Knowledge Discovery in Databases. Research Track and Applied Data Science Track. European Conference, ECML PKDD 2026, Naples, Italy, September 7–11, 2026, Proceedings
Springer, 2027.
This volume is Part VIII of the refereed proceedings of the European Conference on Machine Learning and Knowledge Discovery in Databases, ECML PKDD 2026, held in Naples, Italy, September 7–11, 2026. It contains 40 papers from the Research Track and the Applied Data Science Track and is published as volume 16948 of Lecture Notes in ...
Added: November 9, 2026
Artificial Intelligence for Software Engineering (AI4SE): A Review of Capabilities, Evaluation, and Verification Challenges
Avdoshin S.M., Pesotskaya E.Y., Proceedings of the Institute for System Programming of the RAS 2026 Vol. 38 No. 6, part 2 P. 133–146
Artificial intelligence has significantly reshaped contemporary software engineering practice, changing how software systems are designed, implemented, tested, and maintained. Recent advances in large language models and AI-assisted development tools have expanded the role of AI from supporting isolated tasks to participating in multiple stages of the software lifecycle. In many development settings, software is now created from high-level specifications ...
Added: November 8, 2026
MFL-ScrollNet: Recurrent Sliding-Window Detection for Panoramic Pipeline Magnetic Flux Leakage Images
Aleksei Samarin, Belous F., Торопов А. Г. et al., Technologies 2026 Vol. 14 No. 11 P. 1–21
Abstract Automated interpretation of magnetic flux leakage (MFL) data is central to condition assessment of long-distance oil and gas pipelines. Yet, full-resolution panoramas are difficult to process without either suppressing small anomalies through resizing or fragmenting elongated objects at sliding-window boundaries. We propose MFL-ScrollNet, a recurrent sliding-window detector that formulates panoramic analysis as an ordered sequence ...
Added: November 8, 2026
Proceedings 2026 IEEE International Conference on Joint Cloud Computing JCC 2026
IEEE Computer Society (Conference Publishing Services, CPS), 2026.
Added: November 7, 2026
Detecting the undetectable: benchmarking AI-generated text
Sergey Avdoshin, Elena Pesotskaya, Saleh H. et al., Procedia Computer Science 2026 Vol. 292 P. 1332–1341
The rapid development of generative large language models (LLMs) has intensified the need for reliable methods capable of distinguishing AI-generated text from human writing, especially in academic and professional settings. This paper presents the results of a systematic benchmarking study evaluating the performance and limitations of contemporary LLM-text detectors applied to Russian-language academic content. We introduce ...
Added: November 7, 2026
PrimeKV: Preserving critical KV cache without attention scores for long-context inference
Zhang Z., Ilvovsky D., Neurocomputing 2027 Vol. 710
Efficient management of the Key-Value (KV) cache is essential for deploying large language models (LLMs) in long-context scenarios, where memory requirements often exceed the capacity of resource-constrained hardware. Many existing training-free compression algorithms typically rely on attention-driven heuristics, but exhibit two key limitations. First, they require explicit attention score computation, which is difficult to reconcile ...
Added: November 5, 2026
A Multimodal Framework for Aphasia Severity Classification in Russian
Kolmogorova A., Ekaterina Yavshitz, Margolina A. et al., Association for Computational Linguistics, 2026.
Automatic classification of aphasia severity presents persistent challenges, particularly for languages with limited clinical speech re sources such as Russian. This paper explores a multimodal approach to severity estimation that combines acoustic and semantic representa tions of pathological speech. Acoustic features are extracted using pretrained Wav2Vec 2.0 models, while semantic information is obtained from the ...
Added: November 4, 2026
Findings of the Association for Computational Linguistics: EMNLP 2026
Association for Computational Linguistics, 2026.
Findings of the Association for Computational Linguistics: EMNLP 2026 ...
Added: November 3, 2026
PULSE: Psychological Characteristics Unified Learning via Speech-based Estimation
Abdulkhadirov T., Ryumina E., Ryumin D. et al., Expert Systems with Applications 2026 Vol. 334 P. 1–29
Assessing human psychological characteristics from speech requires models that can jointly capture affective states, expressive behavior, and relatively stable personality traits. However, most existing speech-based frameworks address isolated tasks and use separate task-specific models. This leads to model proliferation and complicates inference in real-world intelligent systems. Unified models are also difficult to develop because few ...
Added: November 3, 2026
Interpretable GNN with Stable Concepts as Neurons
Kuznetsov S., CEUR Workshop Proceedings 2026 Vol. Vol-4247 P. 27–32
A method for constructing interpretable graph neural networks based on an ordered subsets of "interesting" formal concepts is proposed. Interestingness indices for selecting concepts are compared, namely frequency (extent size) and Δ-stability. The experimental results demonstrate that Δ-stability provides superior performance of the generated networks at the inference stage. ...
Added: November 2, 2026
О длине адаптивной различающей последовательности для семейства наблюдаемых автоматов
Бурдонов И. Б., Evtushenko N. V., Косачев А. С., Труды Института системного программирования РАН 2025 Т. 37 № 6-1 С. 7–20
В статье исследуется длина адаптивной различающей последовательности для семейства инициальных полностью определенных наблюдаемых, возможно, недетерминированных автоматов. Приводится верхняя оценка длины такой последовательности и показывается ее достижимость. Обсуждается, каким образом полученные результаты можно применить при построении адаптивных диагностических тестов на основе конечно-автоматной модели. ...
Added: October 31, 2026
К организации системы запросов в распределенной сети с кластерами диаметра не больше 2
Бурдонов И. Б., Evtushenko N. V., Косачев А. С. et al., Труды Института системного программирования РАН 2026 Т. 38 № 4-1 С. 7–24
В статье усовершенствуется предложенная в предыдущей статье авторов модель кластеризованной распределённой сети с опросом, соответствующая сервис-ориентированной архитектуре. Целью опроса является нахождение ближайшего узла, готового оказать требуемую услугу (сервис) как можно раньше. Предлагаемые алгоритмы обеспечивают достижимость узлов, отсутствие дублирования сообщений, и обмен сообщениями с найденным узлом по кратчайшему пути. Кластеризованность сети означает, что в графе сети ...
Added: October 31, 2026
Идентификация финального состояния в автоматах с таймаутами
Твардовский А. С., Бурдонов И. Б., Evtushenko N. V., Труды Института системного программирования РАН 2026 Т. 38 № 4-2 С. 7–22
В статье вводятся понятия установочной и синхронизирующей последовательностей для конечных автоматов с временными ограничениями и таймаутами. Такие последовательности широко используются для идентификации финального состояния исследуемого автомата как при синтезе тестов на основе формальных моделей, так и при обучении конечно-автоматных моделей. Метод синтеза установочных и синхронизирующих последовательностей основан на использовании конечно-автоматной абстракции временного автомата, поскольку методы ...
Added: October 31, 2026
К организации системы запросов в распределенной сети с кластерами-кликами
Бурдонов И. Б., Evtushenko N. V., Косачев А. С. et al., Труды Института системного программирования РАН 2026 Т. 38 № 3-1 С. 7–32
В статье предложена модель кластеризованной распределённой сети для обработки запросов. В такой сети узлы являются вычислительными единицами, и каждый узел может запросить ту или иную услугу, которая может быть оказана каким-то другим, но заранее неизвестным, узлом сети. Для этого осуществляется опрос сети аналогичный поиску в ширину для того, чтобы найти ближайший узел с необходимыми свойствами. ...
Added: October 31, 2026
Кластеризация услуг распределенной системы, в которой хосты могут выполнять функцию коммутации сообщений
Бурдонов И. Б., Evtushenko N. V., Косачев А. С. et al., Труды Института системного программирования РАН 2025 Т. 37 № 5 С. 7–32
Статья является продолжением предыдущей статьи авторов, в которой строится абстрактная модель распределенной сети, содержащей только хосты и коммутаторы. Хосты предлагают пользователям пакеты определенных услуг (сервисов), сообщения (запросы) между хостами пересылаются через промежуточные узлы по правилам коммутации, и настройка узлов определяет множество путей от хоста к хосту, по которым будут пересылаться пакеты. Ситуация моделируется с использованием ...
Added: October 30, 2026
Модель распределенной системы, в которой хосты могут выполнять функцию коммутации сообщений.
Бурдонов И. Б., Evtushenko N. V., Косачев А. С. et al., Труды Института системного программирования РАН 2025 Т. 37 № 4-1 С. 7–30
В работе строится абстрактная модель распределенной сети, содержащей только хосты и коммутаторы, которая позволяет оценить классы задач, которые необходимо решать в такой сети, принимая во внимание, в том числе, нефункциональные параметры. Предполагается, что хосты предлагают пакеты определенных услуг (сервисов) и сообщения (запросы) между хостами пересылаются через промежуточные узлы по правилам коммутации. Правило определяет, каким соседним ...
Added: October 30, 2026
Improving system survivability by path duplication
Бурдонов И. Б., Evtushenko N. V., Косачев А. С., Programming and Computer Software 2025 Vol. 51 No. 4 P. 224–241
In this paper, the problem of distributed network survivability is investigated. A distributed system is modeled by a finite connected undirected graph the nodes of which are divided into two types: hosts and switches. Hosts perform computational functions, while switches are used for message passing between hosts. The survivability of the system is understood as ...
Added: October 30, 2026
Улучшение живучести системы с помощью дублирования путей
Бурдонов И. Б., Evtushenko N. V., Косачев А. С., Программирование 2025 № 4 С. 11–32
Исследуется проблема живучести распределенных сетей. Распределенная система моделируется конечным связным неориентированным графом, вершины которого делятся на два типа: хосты и коммутаторы. Хосты выполняют вычислительные функции, а коммутаторы обеспечивают доставку сообщений между хостами. Под живучестью системы понимается ее способность выполнять свои основные функции по передаче сообщений после выхода из строя некоторых ребер графа. Решение проблемы живучести ...
Added: October 30, 2026
Programming and Computer Software
M.: Pleiades Publishing, Ltd. (Плеадес Паблишинг, Лтд), 2025.
Programming and Computer Software is a peer-reviewed journal devoted to various problems in all areas of computer science: operating systems, compiler technology, software engineering, artificial intelligence, etc. The journal publishes original manuscripts submitted in English, as well as works translated from several other journals. The sources of content are indicated at the article level. The ...
Added: October 30, 2026
Методология создания информационных систем
Karminsky A. M., Chernikov B. V., М.: НИЦ Инфра-М, 2026.
Рассмотрены методологические вопросы создания финансово-экономических информационных систем, проблемы информатизации производственной и дистрибьютерской деятельности, темы адаптации типовых систем в бизнес-структурах, в том числе систем поддержки офисной деятельности. Для студентов учреждений среднего профессионального образования, обучающихся по укрупненным группам специальностей 09.02.00 «Информатика и вычислительная техника», 38.02.00 «Экономика и управление», экономистов, юристов, предпринимателей и финансистов, а также специалистов и ...
Added: October 30, 2026
Mean-field reduction of networks of bursting neurons
Guerreiro I., Sergey Skorokhod, di Volo M. et al., Communications in Nonlinear Science and Numerical Simulation 2027 Vol. 164 Article 110954
The collective dynamics of spiking networks of neurons has been of central interest to both computational neuroscience and network science. Over the past years, a new generation of neural population models based on exact reductions (ER) of spiking networks have been developed. However, most of these efforts have been limited to networks of neurons with simple dynamics (e.g. the ...
Added: October 29, 2026
A Three-Party W-State Quantum Secret Sharing Protocol with X-Gate Encoding and Forbidden-Outcome Detection
Timur Teregulov, Elena R. Loubenets, / Series Quantum Physics "arXiv". 2026. No. 2609.31472.
We develop a new three-party quantum secret-sharing (QSS) protocol based on a three-qubit W state. This protocol encodes the secret-sequence bits using X gates and employs randomly selected Hadamard operations and measurement bases to generate information and security-test rounds. We evaluate the efficiency of the proposed protocol and analyze its security against an internal adversary ...
Added: September 28, 2026
Discovering object-centric Petri nets with parametric arcs
I.I. Sergeev, I.A. Lomazova, Modeling and Analysis of Information Systems 2026 Vol. 33 No. 3 P. 394–419
Object-centric process mining has emerged as a powerful paradigm for analyzing event data involving multiple interacting business objects. Existing discovery techniques often rely on object-centric Petri nets with fixed arc multiplicities, limiting their ability to represent parametric resource consumption and production patterns and to capture quantitative dependencies between interacting object types. In this paper, we ...
Added: September 24, 2026
On calibration of remote sensing retrievals of ecosystem respiration (Reco) with tower measurements over,Russian forests and wetlands
Shabanov N., Kuricheva O., Kurbatova J. et al., / Series Working Papers SSRN "Department of Economics Ca’ Foscari University of Venice". 2026.
The carbon balance of an ecosystem is the difference between Gross Primary Productivity (GPP) and Ecosystem Respiration (Reco) as expressed by Net Ecosystem Exchange (NEE). While remote sensing retrievals of GPP have reached maturity, Reco estimation remains underexplored and ultimately cast bias on NEE. Here we present an end-to-end multi-scale analysis of the mechanism of ...
Added: August 21, 2026
  • 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