MODELING VERIFICATION AND ANALYSIS OF CONCURRENT PROBABILISTIC REVERSIBLE SYSTEMS

• Main Author: ,, ARPIT
• Format: Thesis
• Language: English
• Published: 2015
• Subjects: QA75 Electronic computers. Computer science
• Online Access: http://utpedia.utp.edu.my/21471/1/2015-IT-MODELING%20VERIFICATION%20AND%20ANALYSIS%20OF%20CONCURRENT%20PROBABILISTIC%20REVERSIBLE%20SYSTEMS-ARPIT.pdf; http://utpedia.utp.edu.my/21471/
• Institution: Universiti Teknologi Petronas

This thesis addresses the problem of modeling and analysis of the distributed systems under the probabilistic and reversible environment. On the theoretical side a mathematical model named as Concurrent reversible probabilistic automata (CPRA) is presented here. In this scenario, CPRA implements both internal as well as external non-determinism. CPRA implements reversibility by introducing a memory structure organized in the form of stack. Memories take care of backward synchronization and at the same time maximally flexible. This fact is proved under the consistency of the memories. The resolution of the non-determinism is necessary for the probabilistic analysis which leads to the probabilistic characterization of the traces of the CPRA. Hence, a probability measure space has been constructed on the set of infinite traces of the CPRA. The probability measure space developed here is true irrespective of how non-determinism is resolved.