Maksymets O. Algebraic automata analysis methods of procedural programs and reactive systems

The thesis is devoted to the investigation of program invariant generation and reactive systems properties analysis. Program code models with U-Y-scheme over polynomial ring. Upper and lower approximation methods that generate invariants for U-Y-scheme over a free algebra are adopted for polynomial ring. Conditions and invariants are presented as polynomial of program variables equal to zero. Set of conditions forms an ideal over polynomial ring. Procedure that takes true conditions before assignment and assignment operator and produces all conditions, that are true after assignment is an effect operator. The effect operator for conditions presented as ideals in polynomial ring is built, and theorem about correctness is proved. The effect operator does not require assignment operator to be invertible. Procedure of conditions intersection is derived. Theorem about finite conditions stabilization during method execution is proved. As a result, invariant generation library is developed. Implementation generates valuable nontrivial invariants for procedure programs. Transition system model is chosen as a general model for information system representation. Interaction of such systems is proposed to model with synchronous product of transition systems. Properties of transition systems product are analyzed using Petri nets. Theorem about correspondence between transition systems product and Petri nets model is proved. TSS-method that builds minimal set of solutions for system of linear homogeneous diophantine equations over natural numbers is improved. Truncated set of solutions is built to include equations one by one on each step of the method. As an order of inclusion does not effect the solution set optimal change of the order is proposed. Improvement is based on a procedure of equation selection that minimizes a number of generated solutions on the next step. Improved TSS-method shows good results with sparse incidence matrices of Petri nets. Improved TSS-method is used to find S-invariants and T-invariants of Petri nets and check reachability for free choice Petri nets, unreachability, boundedness for one place, finds traps and deadlock based on derived invariants. Other properties are checked with reachability graph and coverability tree. New technological process based on improved TSS-method for Petri nets properties analysis is presented and implemented, as a standalone library. Procedure of transition system's specification correctness check for Linear Temporal Logic is proposed. The procedure is based on Buchi automata theory.