Dissertation > Excellent graduate degree dissertation topics show

Analysis and Control of Stochastic Real Time Systems

Author: ZhangJunHua
Tutor: HuangZhiQiu
School: Nanjing University of Aeronautics and Astronautics
Course: Applied Computer Technology
Keywords: stochastic real time systems probabilistic timed automata Markov decision process model checking reach-ability counterexample controller synthesis
CLC: TP302.7
Type: PhD thesis
Year: 2011
Downloads: 23
Quote: 0
Read: Download Dissertation


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.

Related Dissertations

  1. Research on the Methods for Detecting Mismatch of Web Services Based on Bounded Model Checking,TP311.52
  2. Study on Hybrid Remanufacturing/Manufacturing Inventory Control System Based on PULL Strategy,F224
  3. Research on a Secure E-Commerce Payment Protocol Based on Four Parties,TP393.08
  4. The Twelfth Five Years Plan of Main Air Pollutants Total Amount Control of Anhui Province and Analysis of Its Attainability,X321
  5. Research on UML Modeling and Model Checking of CTCS-3 Train Control System,TP273
  6. Design and Implementation Automatic Analyzer for Security Protocol,TP393.08
  7. Formal Analysis and Verification of a Transaction Coordination Protocol Named WS-TX for Web Services,TP393.09
  8. Research on Security of E-Commerce Protocols Based on UPPAAL,TP393.08
  9. The Research on Fault Tolerant Multicast in Hypercube Network,TP393.02
  10. Timed automata model - based verification techniques,TP301.1
  11. Research on Insurance Claiming System and Its Coordination Fault-Tolerance Hierarchical Model,TP302.8
  12. Forecasting Model and Applied Research of Based on Time Series ARCH,O211.61
  13. Studies on the Dynamic Simulation Models for Growth of Super Hybrid Rice Seedings,S511
  14. The Monitoring of Farmland Soil Moisture and Water Management System for Cotton on Drip Irrigation under Mulch,S562
  15. Research on Model Checking Algorithms of Ambients Calculi Systems,TP274
  16. Research on Reinforcement Learning Methods for Navigation and Control of Autonoumous Mobile Robots,TP242.6
  17. The Analysis of Model Checking and Verification System of Network Security Protocol,TP393.08
  18. Buffer Overflow Vulnerabilities Detection System Based on Constraint System Model,TP393.08
  19. Research and Implement on Static Malware Detection System Based on Program Semantics,TP393.08
  20. Representation Language of Petri Nets and Reachability Analysis,TP301.1
  21. The Application and Implemenation of PPTL Model Checking Tool,TP311.52

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > General issues > Design and Performance Analysis > Performance analysis, functional analysis
© 2012 www.DissertationTopic.Net  Mobile