?
Prosega/CPN: An Extension of CPN Tools for Automata-based Analysis and System Verification
Proceedings of the Institute for System Programming of the RAS. 2018. Vol. 30. No. 4. P. 107–128.
Carrasquel Gamez J. C., Morales A., Villapol M. E.
This paper presents Prosega/CPN (Protocol Sequence Generator and Analyzer), an extension of CPN Tools for supporting automata-based analysis and verification. The tool implements several operations such as the generation of a minimized deterministic finite-state automaton (FSA) from a CPN’s occurrence graph, language generation, and FSA comparison. The solution is supported by the Simulator Extensions feature whose development has been driven by the need of integrating CPN with other formal methods.
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
Ponomarenko A., / Series Computer Science "arxiv.org". 2025.
This paper addresses the challenge of merging hierarchical navigable small world (HNSW) graphs, a critical operation for distributed systems, incremental indexing, and database compaction. We propose three algorithms for this task: Naive Graph Merge (NGM), Intra Graph Traversal Merge (IGTM), and Cross Graph Traversal Merge (CGTM). These algorithms differ in their approach to vertex selection ...
Added: July 30, 2026
Piontkovski D., / Series arXiv "math". 2026.
A noncommutative projective variety is defined, following Artin and Zhang, by a graded coherent algebra 𝐴. The category of coherent sheaves is then the quotient qgr(𝐴) of the category of finitely presented graded modules by the subcategory of torsion modules. We consider the categorical and polynomial entropies of the Serre twist, that is, of the ...
Added: June 23, 2026
Piontkovski D., / Series arXiv "math". 2025.
If a symmetric multilinear algebra is weakly nil, then it is Engel. This result may be regarded as an infinite-dimensional analogue of the well-known Jacobian theorem, which states that if a polynomial mapping has a polynomial inverse, then its Jacobian matrix is invertible. This refines a theorem of Gerstenhaber and partially answers a question posed ...
Added: June 23, 2026
Shipilov F., Barnyakov A., Ivanov A. et al., / Series Physics "arxiv.org". 2026.
A fast simulation of the detector response is a vital task in high-energy physics (HEP). Traditional Monte-Carlo methods form the backbone of modern particle physics simulation software but are computationally expensive. We present a machine-learning-based approach to fast simulation of the Focusing Aerogel Ring Imaging Cherenkov (FARICH) detector response. Given a particle track and momentum, ...
Added: May 19, 2026
Derkacheva A., Sakirkina M., Kraev G. et al., /. 2026.
Comprehensive data on natural hazards and their consequences are crucial for effective for risk assessment, adaptation planning, and emergency response. However, many countries face challenges with fragmented, inconsistent, and inaccessible data, particularly regarding local-scale events. To address this data gap in Russia, we developed an end-to-end processing pipeline that scrapes news from various online sources, ...
Added: April 28, 2026
Pilé I., Deng Y., Shchur L., / Series arXiv "math". 2026. No. 2604.10254.
We investigate the spatial overlap of successive spin configurations in Markov chain Monte Carlo simulations using the local Metropolis algorithm and the Svendsen-Wang and Wolff cluster algorithms. We examine the dynamics of these algorithms for two models in different universality classes: the Ising model and the Potts model with three components. The overlap of two ...
Added: April 20, 2026
Gabdullin N., Androsov I., / Series Computer Science "arxiv.org". 2026.
Label prediction in neural networks (NNs) has O(n) complexity proportional to the number of classes. This holds true for classification using fully connected layers and cosine similarity with some set of class prototypes. In this paper we show that if NN latent space (LS) geometry is known and possesses specific properties, label prediction complexity can ...
Added: April 2, 2026
Sorokin K., Beketov M., Онучин А. et al., / arxiv.org. Серия cs.SI "Social and Information Networks ". 2025.
Community detection in complex networks is a fundamental problem, open to new approaches in various scientific settings. We introduce a novel community detection method, based on Ricci flow on graphs. Our technique iteratively updates edge weights (their metric lengths) according to their (combinatorial) Foster version of Ricci curvature computed from effective resistance distance between the ...
Added: January 15, 2026
Petrovanov I., Sergeev A., / Series Computer Science "arxiv.org". 2025. No. 2512.18332.
Transport coding reduces message delay in packet-switched networks by introducing controlled redundancy at the transport layer: original packets are encoded into coded packets, and the message is reconstructed after the first successful deliveries, effectively shifting latency from the maximum packet delay to the -th order statistic. We present a concise, reproducible discrete-event implementation of transport coding in OMNeT++, including ...
Added: December 24, 2025
Hessian-based lightweight neural network for brain vessel segmentation on a minimal training dataset
Меньшиков И. А., Бернадотт А. К., Elvimov N. S., / Series arXie "Statistical mechanics". 2025.
Accurate segmentation of blood vessels in brain magnetic resonance angiography (MRA) is essential for successful surgical procedures, such as aneurysm repair or bypass surgery. Currently, annotation is primarily performed through manual segmentation or classical methods, such as the Frangi filter, which often lack sufficient accuracy. Neural networks have emerged as powerful tools for medical image ...
Added: December 1, 2025
Ковалев Д. Ю., Чебышевский сборник 2025 Т. 26 № 3 С. 113–124
In this paper, an imperative programming language considering some hardware limitations of a computer based on the RV32I instruction set is defined, including its syntax and semantics in a form of Hoare logic. The need for such language comes from the fact that formal proofs conducted for programs in languages not considering hardware limitations cannot ...
Added: November 5, 2025
Julio C. Carrasquel, Irina A. Lomazova, , in: 6th International Conference, TMPA 2021, Tomsk, Russia, November 25–27, 2021, Revised Selected Papers. Tools and Methods of Program AnalysisVol. 1559: CCIS .: Springer, 2024. P. 94–106.
Trading systems are software platforms that support the exchange of securities (e.g., company shares) between participants. In this paper, we present a method to search for deviations in trading systems by checking conformance between colored Petri nets and event logs. Colored Petri nets (CPNs) are an extension of Petri nets, a formalism for modeling of ...
Added: January 31, 2024
Springer, 2024.
This book constitutes the refereed proceedings of the 6th International Conference on Tools and Methods of Program Analysis, TMPA 2021, held in Tomsk, Russia, during November 25–27, 2021.
The 15 full papers and 3 short papers included in this book were carefully reviewed and selected from 45 submissions. They focus on various aspects of application of modern ...
Added: January 31, 2024
Zapryagaev A., / Series arXiv "math". 2022.
Added: December 7, 2022
Champaign: Springer, 2020.
The volume LNCS 12226 constitutes the revised selected papers from the four workshops collocated with the 17th International Conference on Software Engineering and Formal Methods, SEFM 2019. ...
Added: October 20, 2022
Orlova G., Новое литературное обозрение 2019 Т. 157 № 3 С. 26–34
The article is devoted to the design, curation and epistemological repair of the “big formal method” in the anthology of formalism and the Russian avant-garde, edited by Sergei Oushakin. ...
Added: June 19, 2019
Springer, 2018.
This book constitutes the refereed proceedings of the 4th International Conference on Tools and Methods for Program Analysis, TMPA 2017, Moscow, Russia, March 3-4, 2017.
The 12 revised full papers and 5 revised short papers presented together with three abstracts of keynote talks were carefully reviewed and selected from 51 submissions. The papers deal with topics such as ...
Added: November 12, 2018
Berriri A., López J., Kushik N. et al., , in: In Proceedings of the 13th International Conference on Evaluation of Novel Approaches to Software Engineering - Volume 1: ENASE.: SciTePress, 2018. P. 440–446.
oftware Defined Networks (SDNs) and corresponding platforms are expected to be widely used in future generation networks and especially deployed and activated on-demand as agile networking control service components. The correct functioning of SDN platforms must be assured, i.e., such platforms should be thoroughly tested before deployment. After thorough verification of SDN controllers and switches, ...
Added: November 1, 2018
Yenigün H., Nina Yevtushenko, Kushik N., Information Processing Letters 2017 Vol. 127 P. 49–53
In this paper, we address the problem of setting a deterministic Finite State Machine (FSM) to a designated initial state. Differently from other papers, we propose to use adaptive synchronizing sequences (test cases) for this purpose and show that for weakly-connected deterministic complete reduced FSMs the problem of checking the existence of an adaptive synchronizing ...
Added: October 31, 2018
Babkin E., Пономарев Н. О., Бизнес-информатика 2017 Т. 43 № 3 С. 30–40
Enterprise architecture design is a complex process which makes it possible to synchronize the capabilities and needs of business and information technologies (IT). It can be achieved by clarifying the understanding and formalization of the business processes and the interaction of the elements of the system through their formal description. The large number of interacting ...
Added: October 3, 2018
Margaria T., Steffen B., IEEE Computer Society, 2006.
This volume contains the Post-Conference Proceedings of ISoLA 2006, the 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2006), which was held in Paphos, Cyprus on 15th-19th November 2006, sponsored by EASST and in cooperation with the IEEE Technical Committee on Complex Systems. ...
Added: September 30, 2015
Berlin: Springer, 2014.
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 ...
Added: July 3, 2014
Babkin E., Buzueva A., Logvinova K. V., Бизнес-информатика 2014 № 2 С. 33–43
The article analyzes the methods and provides a solution to the problem of detecting logical contradictions in business process models of the health care company. Practical purpose of solving the problem is to increase the efficiency of data management for municipal agencies as stakeholder of company. The methodology is based on formal tools relational logic ...
Added: April 17, 2014