Analysis And Control Of Stochastic Real Time Systems

How to assure the correctness and reliability of computer system is one of the most important tasks for computer researcher and developer. Model checking is a powerful way to uphold it. When people want to model and analysis complex systems, some factors such as non-determinism of event occurring, time constraint of event occurring and cost of finishing jobs should be considered. This is the aim of stochastic real time systems model checking.Stochastic real time systems model checking is an active research field born in 1990's. Now many important theory researches are completed and broad application is realized around the filed. To verify the actions of stochastic real time systems, model checking can be used. If the actions of systems are not satisfied with the demand of property, counterexample can be generated. Furthermore, to control the actions of systems with non-determinism, a controller can be synthesized based on the system model and the requirement, which can then be used to control the system. In this paper, research works have been done on the analysis, diagnosis and control of stochastic real time systems. The typical models of stochastic real time systems are discrete time (continuous time) Markov chain, discrete time (continuous time) Markov decision process, and probabilistic timed automata. In this paper, research works have been done aiming on discrete time (continuous time) Markov decision process, and probabilistic timed automata and its extended models. The concrete works are as follows:1,Model checking is done aiming at the extended models of probabilistic timed automata—priced probabilistic timed automata and interval probabilistic timed automata.(1)While priced probabilistic timed automata is used to model systems, optimal cost under probability lower bound is asked to calculate. Latterly, priced probabilistic timed automaton is extended to a multiple price version, and optimal cost for primary price under probability lower bound and secondary prices upper bound is asked to calculate. For both of above questions, algorithms and examples for verification are presented.(2)Interval probabilistic timed automata is constructed to describe stochastic real time system in which the value of discrete transition probability is an interval. Model checking interval probabilistic timed automata (IPTA) is asked to solve. The key problem is to calculate the maximal probability on the model. Through a reverse breadth-first searching algorithm based on zone, interval Markov decision process with loose condition (LIMDP) is obtained from IPTA. As the equivalence for calculating maximal probability on the two models, we transfer the calculation of the maximal probability on IPTA to LIMDP. The strategy for calculating the maximal probability on LIMDP is designed.2,Counterexample generation is researched on model checking probabilistic timed automata and continuous timed Markov decision process.(1)Counterexample generation for model checking probabilistic timed automata is asked to solve. The definition of above counterexample is given, and a quick way to calculate the above counterexample is presented. Furthermore, after a deep analysis on the previous process, a refined algorithm for generating a counterexample with less testimony is designed.(2)Counterexample generation for reach-ability on continuous time Markov decision process is asked to solve. The definition of above counterexample is given, and efficient steps and algorithms to generate a counterexample are presented. The sorts of schedulers on which above algorithms are depended on are discussed.3,Controller synthesis is researched aiming at discrete time Markov decision process of conflict tolerant specification.A new kind of logic, Conflict-tolerant PCTL* with past operator (CT-PPCTL*) is presented, to denote conflict tolerant specification with probability constraint. The problem of controller synthesis for Markov decision process over CT-PPCTL* is asked to solve. A framework for the solution of the problem is presented.