1. Algebraic programming and insertion modeling
In the early 1970s, Victor Glushkov, head of the Institute of Cybernetics of the Academy of Sciences of Ukraine, founded a computer science school centered on algebraic methods. Research topics ranged from automated theorem proving to algebraic modeling and from scientific concepts to industrial software applications.
The Algebraic Programming System (APS) developed as a part of this research program used a term rewriting technique for formula processing. It was used for the symbolic modeling of specifications presented as an automaton or a transition system. The term rewriting system captures the behavior of the modeled specifications.
In the early 2000s, the APS was extended by incorporating the concept of interaction among transition systems in some algebraic environments. The key idea is an insertion function that defines the behavior of interacting transition systems (called agents) in an algebraic environment. This concept was developed in the context of the IMS.
Behavior algebra and basic protocol specifications are used for the formal description of a model. Algebraic artifacts such as theorems and abstract algorithms provide a basis for formal verification methods. These methods were implemented and successfully applied to industry projects in Motorola, Inc.
The algebraic approach and insertion modeling were efficient for the symbolic modeling of distributed application behavior. It enabled proving or refuting the properties by presenting counterexamples for a system with an arbitrary number of agents. It mapped the main techniques of the model checking community and extended behavior algebra theories specialized for distributed systems with a large degree of concurrency.
By using a formal model of an application at some abstraction level, we can generate different scenarios for the behavior of agents or groups of agents. These scenarios are symbolic and can be instantiated to concrete ones by using formal methods. The generation of symbolic scenarios provides good coverage of behaviors, and therefore, the derived concrete scenarios can be considered as a test suite for created software.
Algebraic matching used in rewriting machines was considered as the main mechanism in security tasks such as the detection of vulnerabilities and intruder attacks.
All these techniques anticipate the usage of solving/proving machines like Z3, cvc, and solvers developed in the scope of IMS.
In recent years, our algebraic approach has been applied for studying the properties of consensus protocols in the development, verification, and testing stages of a distributed system based on blockchain solutions and for analyzing token economies.
2. Insertion modeling method
Insertion modeling focuses on building models and studying the interaction of agents and environments in complex distributed multiagent systems. Informally, the main concepts of the insertion modeling paradigm can be summarized as follows.
1. The world is a hierarchy of environments and agents inserted into these environments.
2. Agents and environments are entities evolving in time and having observed behaviors.
3. The insertion of an agent into an environment modifies the behavior of this environment and creates a new environment into which new agents can be inserted.
4. An environment considered as an agent can be inserted into a higher-level environment.
5. New agents can be inserted into an environment, moving from higher-level ones as well as from internal agents that have already been inserted into the environment before.
6. Agents and environments may model environments and other agents at different abstraction levels.
With regard to mathematical refinements, we choose the notion of the transition system for the agent that is the most abstract mathematical concept and model the system that evolves over time. Thus, an agent is a labeled transition system whose states are defined up to bisimulation or trace equivalence.
A labeled transition system is defined by the set of states and the set of labeled transitions 
Transitions from one state to another are labeled by the actions, and the equivalence of states is the equality of behaviors in these states. In the case of bisimilarity, the behavior is a labeled tree. In the case of trace equivalence, it is a set of sequences of actions (traces), that is, paths of possible evolution of the system.
An environment is an agent that possesses an insertion function. Specifically, an environment is a tuple <E, C, A, Ins>, where E is the set of states of the environment; C, the set of environment actions; A, the set of actions of agents that can be inserted into this environment; and 
an insertion function. Here, F(A) is a complete behavior algebra over a set of actions A (behavior algebra is discussed below). Thus, every environment E admits the insertion of any agent with the set of actions A.
We consider agents as attribute transition systems. In such systems, states are defined by values of attributes. The agents have a set of attributes that define the agent type. Every attribute can be a simple one (integer, enumerated, real) of numeric or symbolic types. An attribute can also be of functional type. Environment attributes are associated with global attributes that are known to all agents.
2.1. Behavior algebra
In 1997, Gilbert and Letichevsky introduced the notion of behavior algebra. It was realized in the scope of the IMS. Behavior algebra is a two-sorted universal algebra. The main sort is a set of behaviors and the second sort is a set of actions. This algebra has two operations, three terminal constants, and an approximation relation. The operations are the prefixing a.u (where a is an action and u is a behavior) and nondeterministic choice of behaviors u + v (associative, commutative, and idempotent operations on the set of behaviors). The terminal constants are successful termination ∆, deadlock 0, and divergent behavior ⊥. The approximation relation ⊑ is a partial order on the set of behaviors with minimal element ⊥. Examples of behavior expressions include the following:
B0 = a1.a2.B1 + a3.B2,
B1 = a4, B2 =…
These imply that behavior B0 could be interpreted as a sequence of actions a1 and a2 followed by behavior B1 or as action a3 followed by behavior B2. Behavior B1 will finish after action a4.
The behavior algebra is also enriched by two operations: parallel (||) and sequential (;) compositions of behaviors.
Behavior algebra expressions can be presented in graphical form. The formalization language is called UCM (Use Case Maps), and it is standardized as a part of URN (User Requirements Notation) in the ITU-T recommendation (Z.151) that provides a scenario-based approach to requirement specification. An example and the list of constructs of this language are shown below.
A UCM is an oriented graph that defines the sequence in which responsibility constructs are performed. The process of performing can be forked for parallel processes using the “and-fork” construct and synchronized using the “and-join” construct. The “or-fork” construct defines one of the alternative paths in the sequence of responsibility constructs. The “stub” construct defines a reference to another UCM.
Behavior algebra operations can be mapped to the UCM. It is used for visualizing the graphical scenario that corresponds to behavior algebra expressions.
2.2. Basic Protocols specifications
Our team developed the Basic Protocols language in the scope of the Verification of Requirements Specifications (VRS) project that was implemented together with Motorola and the Glushkov Institute of Cybernetics. This language is built over some attribute environment in which all agents interact with one another. Every agent is defined by a set of attributes. An agent changes its state under some conditions formed by values of attributes. Every agent’s actions define some basic protocol that is represented by the triple B = <P, A, S>, where P is a precondition of the basic protocol presented as a formula in some basic logic language; S, a postcondition; and A, a process that visualizes the agent transition. As a basic logical language, we consider the set of formulas of first-order logic over polynomial arithmetic. As a whole, the semantic of a basic protocol means that the agent could change its state if the precondition is true and the state will be changed correspondingly to the postcondition, which is also a formula of first-order logic. The postcondition could also contain an assignment statement. The basic protocol process depends on the subject domain and illustrates the sequence of the basic protocol application. In the telecommunications domain, it could involve sending or receiving signals with corresponding parameters. Basic protocol is graphically represented by an MSC (Message Sequence Charts) diagram (see next Fig.). With regard to UCM, basic protocol maps to the responsibility-construct.
2.2. Symbolic modeling
The initial state of agents can be represented by an initial formula. Starting from the initial formula, we can apply the action corresponding to the behavior algebra expression. The action is applicable if its precondition is satisfiable and consistent with the current state. Starting from the formula of the initial state S0 and from the initial behavior B0, we select the action and move to the next behavior. In the first step, we check the satisfiability of the conjunction
S0 /\ Pa1
if B0 = a1.B1, and Pa1 is a precondition of a1. The next state of the environment is obtained by means of the predicate transformer, that is, the function over the current agent state, precondition, and postcondition.
PT(Si, Pai, Qai) = Si+1
By applying the predicate transformer function to different agent states, we can obtain the sequence S0, S1,… of formulas that express the agent states changing from the initial state. We present the trace by the sequence of processes of actions a1, a2,… Every agent state covers the set of concrete agent values, and the process of generating such traces is called symbolic modeling. The predicate transformer has to be defined for the corresponding theory. Our last extension of the predicate transformer theory is to apply it to formulae with quantifiers.