Interactive Markov Chains: Theory And Applications

Interactive Markov chains (IMCs) are concurrent system models with both func-tional specification and performance evaluation. Combining classical process al-gebra models and continuous-time Markov chains (CTMCs) orthogonally, IMCsprovide an elegant compositional performance evaluation framework. In thisthesis, we investigate the theory of IMCs and their applications in the fields ofperformance evaluation and hierarchical system design and analysis. We focuson the following three topics:1. The branching-time equivalences and preorders on IMCs. We define thenotions of strong and weak (bi)simulations on the classical functional andperformance models of concurrency in a uniform framework. The logi-cal characterizations of these branching-time equivalences and preorders,i.e., the relations to the logical equivalences, are also studied based on anaction-based logic aCSL. By investigating the interrelations among theseequivalences and preoders, we obtain a branching-time equivalences spec-trum for IMCs. This spectrum subsumes the corresponding results on theclassical functional and performance models.2. Model checking for IMCs. The main purpose of IMCs is to propose acompositional performance evaluation model. We therefore investigate themodel checking algorithm for IMCs to provide an automatic and e?cientmethod for the performance evaluation of large and complex systems. Weuse aCSL as the specification language of properties and put forward afully action-based model checking algorithm. In association with the com-positional modeling power of IMCs, this method has potential applicationto evaluating large and complex systems. The presented algorithm is anextension of model checking pure continuous-time Markov chains and co-incides with the original one. When an IMC reduces to a CTMC, ouralgorithm just reduces to the model checking algorithm on CTMCs. As atrial, we have implemented a prototype of the algorithm in C and use it todemonstrate how to apply this method to the auto performance evaluationof action-based systems.3. Action refinement for IMCs. As a classical hierarchical design method-ology, we also apply the theory of action refinement to the framework ofIMCs. We adopt the viewpoint of modeling action refinement as an opera-tor and investigate both syntactic and semantic action refinement of IMCs.We prove that the semantic action refinement behaves well. Two com-monly used equivalences, a linear-time interleaving trace equivalence and abranching-time interleaving bisimulation equivalence, are both congruencesunder the semantic action refinement. For syntactic action refinement, weshow that only for safe syntactic action refinement the two aforementionedequivalences are congruences due to IMCs are interleaving concurrent mod-els. Therefore, the syntactic and semantic action refinement coincide underthese equivalences only when they are both safe.