Automata for Modeling Reversible Probabilistic Processes

Abstract:

This paper presents a construction of an automaton that aids the modeling of probabilistic processes which exhibit reversibility during their computations. A probabilistic process defines a probability distribution over the uncertainties of its computations. This characteristic also makes them distinct from nondeterministic processes. But, uncertainties hinder the assurance about the quality of such systems gained by the traditional testing methods. Further, reversibility acts as a catalyst in such scenarios by raising the possibility of achieving the states which were inaccessible in past. Thus, the verification of such systems is necessary and this requires the system to be formally specified. In this respect, proposed work provides the constructs for modeling probabilistic environments and reversibility. Former is achieved by the introduction of discrete probabilities in classical automata theory, and later is implemented by giving the constructs of memory. It also provides the constructs for representing non-determinism by specifying the choices over several probability mass functions for a state.

• Periodical: Applied Mechanics and Materials (Volume 422)
• Pages: 185-190
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.422.185
• Online since: September 2013
• Authors: Arpit Arpit, Afza Shafie, Wan Fatima Wan Ahmad
• Keywords: Automata, Formal Specification, Formal Verification, Non-Determinism, Parallel Composition, Probability

References

[1] Shigong, Long & Lijun, Wang. 2010. Analysis of cryptographic protocols using LTL of knowledge. In Proceedings of Networking and Digital Society, pp.463-466.

DOI: 10.1109/icnds.2010.5479238

[2] Alfaro, Luca De. 1988. Formal verification of probabilistic systems. In PhD thesis: Stanford University, Stanford, CA, USA.

[3] Glabbeek, R.J.V., Smolka S.A. & Steffen, B. 1990. Reactive, generative, and stratified models of probabilistic processes. In Information and Computation, 121(1): pp.130-141.

DOI: 10.1006/inco.1995.1123

[4] Sokolova, A. & Vink, E.P. De. 2004. Probabilistic automata: System types, parallel composition and comparison. In Springer, Validation of Probabilistic Systems : A Guide to Current Research, pp.1-43.

DOI: 10.1007/978-3-540-24611-4_1

[5] Hartog, J.I. den. & Vink, E.P. de. 1999. Mixing up nondeterminism and probability: a preliminary report. In Electronic Notes in Theoretical Computer Science, 22(0): pp.88-110.

DOI: 10.1016/s1571-0661(05)82521-6

[6] Segala, R. 1996, Modeling and verification of randomized distributed real-time systems. In Technical report: Cambridge, MA, USA.

[7] Marats, Golovkins. & Maksim, Kravtsev. 2001. Probabilistic reversibility and its relation to quantum automata: R-trivial Idempotent Languages. In Proceeding of International Symposium, pp.351-363.

DOI: 10.1007/978-3-642-22993-0_33

[9] Marats, Golovkins., Maksim, Kravtsev. & Vasilijs, Kravcevs. 2009. On a class of languages recognizable by probabilistic reversible decide-and-halt automata. In Theor. Comput. Sci, 410(20): 1942-(1951).

DOI: 10.1016/j.tcs.2009.01.042

[10] Phillips, Iain. & Irek, Ulidowski. 2007. Reversibility and models for concurrency. In Theor. Comput. Sci, 192(1): 93-108.

[11] Shengang, Hao. & Zhang, Li. 2010. Dynamic Web Services Composition CONCLUSION AND FUTURE WORK based on Linear Temporal Logic. In Proceedings of International Conference of information Science and Management Engineering: pp.122-127.

DOI: 10.1109/isme.2010.87

[12] Pnueli, A. 1977. The temporal logic of programs. In proceedings of IEEE Symposium Foundations of Computer Science, pp.46-57.

[13] Jianli, Ma., Dongfang, Zhang., Guoai, Xu. & Yixian, Yang. 2010. Model Checking Based Security Policy Verification and Validation. In Proceedings Intelligent Systems and Applications, pp.1-4.

DOI: 10.1109/iccet.2010.5486002