Research On Model Detection Theory Based On Automata And Possibility Kripke Structure

Society is increasingly dependent on dedicated computer and software systems to assist us in almost every aspect of daily life. For instance, mobile phones, communication systems, medical devices, audio and video systems, and consumer electronics in general are containing vast amounts of software. A common pattern is the constantly increasing complexity of systems, a trend which is accelerated by the adaptation of wired and wireless networked solutions. Therefore, a main challenge for the field of computer science is to provide formalisms, techniques, and tools that will enable the efficient design of correct and well-functioning systems despite their complexity. Over the last two decades or so a very attractive approach toward the correctness of computer-based control systems is that of model checking. So, what exactly is model checking? We defined it in different ways:1. Model checking, a prominent formal verification technique for assessing functional properties of information and communication systems;2. Model checking allows for desired behavioral properties of a given system to be verified on the basis of a suitable model of the system through systematic inspection of all states of the model.With the advancement of science and technology, model checking technique has a sustained development from the original classic model checking to probabilistic model checking, and then to today’s multi-valued model checking, quantum model checking and possibilistic model checking. Many experts and scholars have made a lot of research on this formal verification technique both in theory and practice. It is essential for us to know how to apply model checking theory to practice and thus solve practical problems. A formal model based on automata is used to describe scheduling algorithm for multiprocessor systems.Cost (or dually as bonus) is the crucial factor in the decision-making systems. We give the notion of possibilistic Kripke cost structure (PoKCS), and consider expected measures and multi-attribute decision making problems on PoKCS.The main contents of this thesis are as follows:(1) A formal model based on extended Buchi automata is proposed, and the model is used to describe the TDS (Task Duplication based Scheduling) algorithm. The expected properties of the algorithm are described by Linear Temporal Logic formulas and verified on the above model.(2) The aim of this part is to consider an extension of possibilistic Kripke structure, called possibilistic Kripke cost structure (PoKCS), and consider expected measures and multi-attribute decision making problem on PoKCS. A possibilistic Kripke cost structure is a possibilistic Kripke structure in which transitions (or states) are augmented with costs, natural numbers that can be interpreted as costs, or dually as bonuses. We consider equipping transitions with costs. For convenience, we will give a case and apply the theories in this thesis to solve the problems about management decision of project.