KeYmaera is an interactive theorem prover and is used to verify safety properties of cyber-physical systems (CPSs). It implements a Dynamic Logic for Hybrid Programs (HPs), while a HP models a CPS very precisely. Verifying properties of a given system in KeYmaera can become a challenge for a user since the proof is authored in a classical sequent calculus framework and a successful proof requires from the user intimate knowledge of the available calculus rules. Another barrier for widespread application of KeYmaera is the purely textual representation of current proof goals, what requires from the user very good training, experience, and patience. In this paper, we present an alternative verification approach based on KeYmaera, which drastically improves usability and minimizes user interaction. The main idea is to let the user annotate invariants and contracts to states of the hybrid automaton. Thus, the user can employ the graphical representation of the modelled system and is not bound to the purely textual form of hybrid programs as in KeYmaera. Based on the user-provided contracts, one can generate proof obligations, which are much simpler than the original proof goal in KeYmaera. The article is published in the authors’ wording.

Nowadays, the methods of program-targeted management for the development of various socio-economic systems of complex structure, such as agricultural areas, have become universal. Therefore, the current tasks at hand are the verification of already created development programs and the development of "proper" programs for the development of such systems, by analogy with the verification and development of proper computer programs through developed disciplines in theoretical programming. In this paper, in order to solve the problem of verification of development programs for agricultural territories, a structural scheme of the program is first constructed, through which the axiomatic theory is created, using Hoare’s algorithmic logic system. The main problem in the construction of the axiomatic theory is the development of the axioms of the theory reflecting the preconditions and effects of the implementation of meaningful actions indicated in the text of the development program. The verification of the development program corresponds to the probability of some Hoare triplet, according to the initial and target conditions of the program. For the task of elaboration of the right development programs, the mechanism for constructing a domain model using the PDDL family description languages is described. The description of a specific model is purely declarative in nature and consists of descriptions of predicates and actions of the chosen subject area. In this paper, it is shown how on the described model with the help of intelligent planners, including temporal planners such as OPTIC, solutions to the targets of development programs can be automatically built. Based on expert knowledge and activity standards, a model of an agricultural territory is constructed, a brief description of which is given in the work. The conducted experiments showed the effectiveness of the proposed approach for the development of proper development programs. 

During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invariant synthesis are heuristic ones. This impedes its application. An alternative is the symbolic method of loop invariant elimination suggested by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect in a symbolic form and allows to introduce an inference rule which uses no invariants in axiomatic semantics. This work represents the further development of this method. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes the verification method of iterations over changeable arrays possibly with loop exit in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule was implemented in verification conditions generator which is a part of the automated system of C-light program verification. To prove verification conditions automatically in ACL2, two algorithms were developed and implemented. The first one automatically generates the replacement operation in ACL2 language, the second one automatically generates auxiliary lemmas which allow to prove the obtained verification conditions in ACL2 successfully in automatic mode. An example which illustrates the application of the mentioned methods is described.

One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. The behaviour of such a reactive system displays itself in the correspondence between flows of control signals and compositions of basic actions performed by the system. We believe that the behaviour of this kind requires more suitable and expressive means for formal specifications than the conventional LT L. In this paper, we define some new (as far as we know) extension LP-LT L of Linear Temporal Logic specifically intended for describing the properties of transducers computations. In this extension the temporal operators are parameterized by sets of words (languages) which represent distinguished flows of control signals that impact on a reactive system. Basic predicates in our variant of the temporal logic are also languages in the alphabet of basic actions of a transducer; they represent the expected response of the transducer to the specified environmental influences. In our earlier papers, we considered a model checking problem for LP-LT L and LP-CT L and showed that this problem has effective solutions. The aim of this paper is to estimate the expressive power of LP-LT L by comparing it with some well known logics widely used in the computer science for specification of reactive systems behaviour. We discovered that a restricted variant LP-1-LT L of our logic is more expressive than LTL and another restricted variant LP-n-LT L has the same expressive power as monadic second order logic S1S.

In this paper, we investigate the safety of unary inflationary fixed point operators (IFPoperators). The safety is a computability in finitely many steps. IFP-operators exactly correspond to recursive SQL-queries hence this problem has a value for database theory. The problem appears from the fact that if recursive queries contain universe functions and relations, then its execution can fall into an infinite loop. Moreover, universal computational devices (Turing machines et al.) can be modelled by such queries. Hence the problem of the finite computability for such queries is undecidable. In our previous works we established some properties of a universe which imply the finite computability of all IFP-operators in the universe. Here, we investigate a connection between an arity of IFP-operators and their safety. We prove that some results for general IFP-operators don’t hold for unary ones. We construct a universe where all unary unnesed IFP-operators are safe. But in this universe there exist unsafe nested unary IFP-operators and unsafe unnested binary IFP-operators. This differs from general IFP-operators because in general case the safety of all unnesed IFP-operators implies the safety of all IFP-operators. Also there exist elementary equivalent universes where some unary unnesed IFPoperators become unsafe. For general IFP-operators it is also impossible.

A polyprogram is a generalization of a program which admits multiple definitions of a single function. Such objects arise in different transformation systems, such as the Burstall-Darlington framework or equality saturation. In this paper, we introduce the notion of a polyprogram in a non-strict first-order functional language. We define denotational semantics for polyprograms and describe some possible transformations of polyprograms, namely we present several main transformations in two different styles: in the style of the Burstall-Darlington framework and in the style of equality saturation. Transformations in the style of equality saturation are performed on polyprograms in decomposed form, where the difference between functions and expressions is blurred, and so is the difference between substitution and unfolding. Decomposed polyprograms are well suited for implementation and reasoning, although they are not very human-readable. We also introduce the notion of polyprogram bisimulation which enables a powerful transformation called merging by bisimulation, corresponding to proving equivalence of functions by induction or coinduction. Polyprogram bisimulation is a concept inspired by bisimulation of labelled transition systems, but yet it is quite different, because polyprogram bisimulation treats every definition as self-sufficient, that is a function is considered to be defined by any of its definitions, whereas in an LTS the behaviour of a state is defined by all transitions from this state. We present an algorithm for enumerating polyprogram bisimulations of a certain form. The algorithm consists of two phases: enumerating prebisimulations and converting them to proper bisimulations. This separation is required because polyprogram bisimulations take into account the possibility of parameter permutation. We prove correctness of this algorithm and formulate a certain weak form of its completeness. The article is published in the author’s wording.

Transformation-based program verification was a very important topic in early years of theory of programming. Great computer scientists contributed to these studies: John McCarthy, Amir Pnueli, Donald Knuth ... Many fascinating examples were examined and resulted in recursion elimination techniques known as tail-recursion and co-recursion. In the paper, we examine just a single example (but new we hope) of recursion elimination via program manipulations and problem analysis. The recursion pattern of the example matches descending dynamic programming but is neither tail-recursion nor corecursion pattern. Also, the example may be considered from different perspectives: as a transformation of a descending dynamic programming to ascending one (with a fixed-size static memory), or as a proof of the functional equivalence between recursive and iterative programs (that can later serve as a casestudy for automatic theorem proving), or just as a fascinating algorithmic puzzle for fun and exercising in algorithm design, analysis, and verification. The article is published in the author’s wording.

Hypergraphic automata are automata with state sets and input symbol sets being hypergraphs which are invariant under actions of transition and output functions. Universally attracting objects of a category of hypergraphic automata are automata Atm(H₁,H₂). Here, H₁ is a state hypergraph, H₂ is classified as an output symbol hypergraph, and S = EndH₁ × Hom(H₁,H₂) is an input symbol semigroup. Such automata are called universal hypergraphic automata. The input symbol semigroup S of such an automaton Atm(H₁,H₂) is an algebra of mappings for such an automaton. Semigroup properties are interconnected with properties of the algebraic structure of the automaton. Thus, we can study universal hypergraphic automata with the help of their input symbol semigroups. In this paper, we investigated a representation problem of universal hypergraphic automata in their input symbol semigroup. The main result of the current study describes a universal hypergraphic automaton as a multiple-set algebraic structure canonically constructed from autonomous input automaton symbols. Such a structure is one of the major tools for proving relatively elementary definability of considered universal hypergraphic automata in a class of semigroups in order to analyze interrelation of elementary characteristics of universal hypergraphic automata and their input symbol semigroups. The main result of the paper is the solution of this problem for universal hypergraphic automata for effective hypergraphs with p-definable edges. It is an important class of automata because such an algebraic structure variety includes automata with state sets and output symbol sets represented by projective or affine planes, along with automata with state sets and output symbol sets divided into equivalence classes. The article is published in the authors' wording.

A model of neural association of three pulsed neurons with a delayed broadcast connection is considered. It is assumed that the parameters of the problem are chosen near the critical point of stability loss by the homogeneous equilibrium state of the system. Because of the broadcast connection the equation corresponding to one of the oscillators can be detached in the system. The two remaining impulse neurons interact with each other and, in addition, there is a periodic external action, determined by the broadcast neuron. Under these conditions, the normal form of this system is constructed for the values of parameters close to the critical ones on a stable invariant integral manifold. This normal form is reduced to a four-dimensional system with two variables responsible for the oscillation amplitudes, and the other two, defined as the difference between the phase variables of these oscillators with the phase variable of the broadcast oscillator. The obtained normal form has an invariant manifold on which the amplitude and phase variables of the oscillators coincide. The dynamics of the problem on this manifold is described. An important result was obtained on the basis of numerical analysis of the normal form. It turned out that periodic and chaotic oscillatory solutions can occur when the coupling between the oscillators is weakened. Moreover, a cascade of bifurcations associated with the same type of phase rearrangements was discovered, where a self-symmetric stable cycle alternately loses symmetry with the appearance of two symmetrical cycles. A cascade of bifurcations of doubling occurs with each of these cycles with the appearance of symmetric chaotic regimes. With further reduction of the coupling parameter, these symmetric chaotic regimes are combined into a self-symmetric one, which is then rebuilt into a self-symmetric cycle of a more complex form compared to the cycle obtained at the previous step. Then the whole process is repeated. Lyapunov exponents were calculated to study chaotic attractors of the system.