State identification is the well-known problem in the theory of Finite State Machines (FSM) where homing sequences (HS) are used for the identification of a current FSM state, and this fact is widely used in the area of software and hardware testing and verification. For various kinds of FSMs, such as partial, complete, deterministic, non-deterministic, there exist sufficient and necessary conditions for the existence ofpreset and adaptive HS and algorithms for their derivation. Nowadays timed aspects become very important for hardware and software systems and for this reason classical FSMs are extended by clock variables. In this work, we address the problem of checking the existence and derivation of homing sequences for FSMs with timed guards and show that the length estimation for timed homing sequence coincides with that for untimed FSM. The investigation is based on the FSM abstraction of a Timed FSM, i.e. on a classical FSM which describes behavior of corresponding TFSM and inherits some of its properties. When solving state identification problems for timed FSMs, the existing FSM abstraction is properly optimized.

Sequential reactive systems include hardware devices and software programs which operate in continuous interaction with the external environment, from which they receive streams of input signals (data, commands) and in response to them form streams of output signals. Systems of this type include controllers, network switches, program interpreters, system drivers. The behavior of some reactive systems is determined not only by the sequence of values of input signals, but also by the time of their arrival at the inputs of the system and the delays in computing the output signals. These aspects of reactive system computations are taken into account by real-time models of computation which include, in particular, realtime finite state machines (TFSMs). However, in most works where this class of real-time automata is studied a simple variant of TFSM semantics is used: the transduction relation computed by a TFSM is defined so that the elements of an output stream, regardless oftheir timestamps, follow in the same order as the corresponding elements ofthe input stream. This straightforward approach makes the model easier to analyze and manipulate, but it misses many important features of real-time computation. In this paper we study a more realistic semantics of TFSMs and show how to represent it by means of Labeled Transition Systems. The use of the new TFSM model also requires new approaches to the solution of verification problems in the framework of this model. For this purpose, we propose an alternative definition of TFSM computations by means of Labeled Transition Systems and show that the two definitions of semantics for the considered class of real-time finite state machines are in good agreement with each other. The use of TFSM semantics based on Labeled Transition Systems opens up the possibility of adapting well known real-time model checking techniques to the verification ofsequential reactive systems.

We address the formal verification of the control software of critical systems, i.e., ensuring the absence of design errors in a system with respect to requirements. Control systems are usually based on industrial controllers, also known as Programmable Logic Controllers (PLCs). A specific feature of a PLC is a scan cycle: 1) the inputs are read, 2) the PLC states change, and 3) the outputs are written. Therefore, in order to formally verify PLC, e.g., by model checking, it is necessary to describe the transition system taking into account this specificity and reason both in terms of state transitions within a cycle and in terms of larger state transitions according to the scan-cyclic semantics. We propose a formal PLC model as a hyperprocess transition system and temporal cycle-LTL logic based on LTL logic for formulating PLC property. A feature of the cycle-LTL logic is the possibility of viewing the scan cycle in two ways: as the effect of the environment (in particular, the control object) on the control system and as the effect of the control system on the environment. For both cases we introduce modified LTL temporal operators. We also define special modified LTL temporal operators to specify inside properties of scan cycles. We describe the translation of formulas of cycle-LTL into formulas of LTL, and prove its correctness. This implies the possibility ofmodel checking requirements expressed in logic cycle-LTL, by using well-known model checking tools with LTL as specification logic, e.g., Spin. We give the illustrative examples of requirements expressed in the cycle-LTL logic.

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 result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.

Multiagent algorithm is a knowledge-based distributed algorithm that solves some problems by means of cooperative work of agents. From an individual agent's perspective, a multiagent algorithm is a reactive and proactive knowledge/believe-based rational algorithm aimed to achieve an agent's own desires. In the paper we study a couple of knowledge-based multiagent algorithms. One particular algorithm is for a system consisting of agents that arrive one by one (in a non-deterministic order) to a resource center to rent (for a while) one of available desired resources. Available resources are passive, they form a cloud; each of the available resources is lent on demand if there is no race for this resource and returns to the cloud after use. Agents also form a cloud but leave the cloud immediately when they rent a desired resource. The problem is to design a knowledge-based multiagent algorithm, which allows each arriving agent eventually to rent some of desired resources (without race for these resources).

The extent of formal verification methods applied to industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs' application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes.

In this paper we consider the software architecture of InnoChain, a distributed ledger system (DLS) with 5 levels of formal verification, including a formally-verified underlying operating system (OS). The objective of this architecture is to achieve a higher level of DLS dependability compared to more traditional software architectures and quality assurance (QA) methods. The architecture of InnoChain includes (1) a programming language for smart contracts which is a domain-specific language with formal semantics embedded into CakeML, which is a functional language ofthe ML family; this allows us to carry out formal verification of smart contracts' correctness properties using higher-order logic systems, such as HOL4; (2) trusted compilation of smart contracts into the machine code using the verified compiler available for CakeML, rather than relying on a virtual machine for execution of smart contracts; (3) using CakeML for implementation of InnoChain node functionality which allows for formal verification of code correctness and trusted compilation into the machine code; (4) formal verification of the consensus protocol used InnoChain, namely HotStuff BFT; (5) using seL4, a formally-verified microkernel, as the underlying OS for InnoChain instead of more traditional general-purpose OSes such as Linux. The proposed verified architecture will allow InnoChain to be used in mission-critical applications, such as the decentralized Aircraft Fuelling Control System which is currently under development for JSC Aeroflot, the Russian national air carrier.

Self-adjustment of parameters can significantly improve the performance of evolutionary algorithms. A notable example is the (1 + (λ,λ)) genetic algorithm, where adaptation of the population size helps to achieve the linear running time on the OneMax problem. However, on problems which interfere with the assumptions behind the self-adjustment procedure, its usage can lead to the performance degradation. In particular, this is the case with the “one-fifth rule” on problems with weak fitness-distance correlation.
We propose a modification of the “one-fifth rule” in order to have less negative impact on the performance in the cases where the original rule is destructive. Our modification, while still yielding a provable linear runtime on OneMax, shows better results on linear function with random weights, as well as on random satisfiable MAX-3SAT problems.

The author regrets that in the original list the references [3] and [4] are in the wrong places and they should be rearranged. In addition, [3] has the wrong article title. The corrected reference list is shown below.
The author would like to apologize for an inconvenience caused.
References
[1] A. I. Mal'tsev, “Constructive algebras I”, Russian Mathematical Surveys, vol. 16, no. 3, pp. 77-129, 1961.
[2] A. I. Mal'tsev, Algoritmy i rekursivnye funktsii. Moscow: Nauka, 1965, In Russian.
[3] R. M. Robinson, “Primitive recursive functions”, Bulletin of the American Mathematical Society, vol. 53, no. 10,pp. 925-942, 1947.
[4] J. Robinson, “General recursive functions”, Proceedings of the American Mathematical Society, vol. 1, no. 6,pp. 703-718, 1950.
[5] V. A. Sokolov, “Ob odnom klasse tozhdestv v algebre Robinsona”, in 14-ya Vsesoyuznaya algebraicheskaya konferentsiya: tezisy dokladov, In Russian, vol. 2, Novosibirsk, 1977, pp. 123-124.
[6] P. M. Cohn, Universal Algebra. New York, Evanston, and London: Harper & Row, 1965.
[7] A. Robinson, “Equational logic for partial functions under Kleene equality: a complete and an incomplete set of rules”, The Journal of Symbolic Logic, vol. 54, no. 2, pp. 354-362, 1989.