Approximate Reasoning—Investigation Of Polynomial Algebraic Dynamic Logic

Complex systems, such as rail traffic systems, aerospace systems, industrial con-trol systems etc., are growing in scale and functionality with the rapid development of computer technology. Because of this increase in complexity, the likelihood of subtle errors and bugs becomes greater. Moreover, any small error may cause catastrophic loss of money, or even human life. It has attracted much attention of researchers in academia and industry how to assure the correctness of designs of complex systems. It has been shown by some research results that the formal method based on logical reasoning may be a proper solution to this problem.Since complex systems are characterized by data flow, continuous states and perfor-mance indices, new challenges arise in reasoning about these systems with logical method-s. These challenges lie in the construction of a uniform logical framework for specifying systems behaviors and properties, supporting compositional and hierarchical verification, the combination of logical reasoning with mathematical procedures and the criteria for measuring properties of complex systems. This thesis focuses on these challenges and makes a thorough study of logical languages, mathematical models, proof systems and approximate reasoning systems for specifying and verifying complex system. The main results achieved are listed as follows:(1) Polynomial algebraic dynamic logic (ADL) is proposed, which effectively solves the problem of constructing a uniform logical framework for specifying system be-haviors and properties. ADL also supports compositional and hierarchical specifi-cation. Under the framework of ADL, system behaviors are described as polyno-mial algebraic programs and property assertions are described as ADL formulas. Compositional specification is supported by the compositional structures of poly-nomial algebraic programs which are obtained by combining small programs with sequential connective, conditional connective, loop connective etc. Hierarchical specification means that the relation between hierarchies of systems is specified as ADL formulas. For instance, the modal formula [a]φ→[β]φ means that system β is implemented by a.(2) Polynomial algebraic transition system (ATS), which is a finer mathematical model, is proposed and effectively solves the problem of describing data flow and contin-uous states. By allowing continuous variables ATS is able to describe continuous states and makes the state space of systems continuous which leads to stronger ex-pressive power. By labeling system transitions with polynomial expressions ATS is able to describe state transitions and data flow which leads to specify finer system behaviors. It makes more sense that mathematical procedures are applicable to the verification and analysis of complex systems by connecting system behaviors and zeros of polynomials.(3) Formal semantics and proof system (ADL calculus) are constructed for ADL, which effectively solve the problem of combination of logical reasoning with mathemat-ical procedures. The semantics of ADL, which is built on ATS, consists of the transition semantics of polynomial algebraic programs and the satisfaction of ADL formulas. Since the transition semantics and satisfaction are defined with zeros of polynomials, the logical implication of formulas can be decided with methods of symbolic computation. Furthermore, ADL calculus is sound and partly complete.(4) Metric semantics and approximate reasoning system are constructed for ADL, which effectively solve the problem of system performance evaluation. The metric semantics is a quantitative extension of formal semantics and evaluates the possi-bility that a property is satisfied by a given state. Approximate reasoning system consists of a collection of metric rules which evaluate the possibility that a formula is valid. Furthermore, approximate reasoning is sound and extends quantitatively the proof system which means that any provable formula in ADL calculus is derived in approximate reasoning system.In the last part of the thesis, two simple cases are verified and analyzed which demonstrate that the approach proposed in the thesis is capable of specifying, verifying and analyzing properties of complex systems.