Abstract
In this paper, a turn-based probability epistemic game structure (TPEGS) is proposed to model knowledge preconditions for actions of system and environment firstly, which is an extension of turn-based synchronous game structures with probabilistic transition. Secondly, we introduce probability operator \( P_{\sim \lambda } \) into alternating temporal epistemic logic (ATEL) and define turn-based probability alternating-time temporal epistemic logic (tPATEL) for model checking the properties of TPEGS quantitatively. The probability of agents knowing some precondition before they implement an action can be expressed in tPATEL. Thirdly, we propose a method to compute probability for model checking verification problems of tPATEL based on DTMC and CTMC, and then analyze the time complexity of the method. Then, we are able to convert a part of tPATEL verification problems into the PATL ones by defining the knowledge formula \( K_{a} \phi ,\, E_{As} \phi \) and \( C_{As} \phi \) as atomic propositions. Finally, we study a flight procedure in STAS using PRISM-games to demonstrate the applicability of the above model checking framework and expand the application field of model checking.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Allen, J.F.: Planning as temporal reasoning. In: KR 1991, pp. 3–14 (1991)
Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM (JACM) 49(5), 672–713 (2002)
Baier, C., Katoen, J.-P., Hermanns, H.: Approximative symbolic model checking of continuous-time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–161. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48320-9_12
Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 315–330. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_22
Chen, T., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: an application to autonomous urban driving. In: 10th International Conference on Quantitative Evaluation of SysTems (QEST 2013). IEEE CS Press (2013)
Delgado, C., Benevides, M.: Verification of epistemic properties in probabilistic multi-agent systems. In: Braubach, L., van der Hoek, W., Petta, P., Pokahr, A. (eds.) MATES 2009. LNCS (LNAI), vol. 5774, pp. 16–28. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04143-3_3
Dowek, G., Munoz, C., Carreno, V.A.: Abstract model of the SATS concept of operations: initial results and recommendations (2004)
Fagin, R., Halpern, J.Y., Megiddo, N.: A logic for reasoning about probabilities. Inf. Comput. 87(1), 78–128 (1990)
Dannenberg, F., Hahn, E.M., Kwiatkowska, M.: Computing cumulative rewards using fast adaptive uniformisation. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 33–49. Springer, Heidelberg (2013a). https://doi.org/10.1007/978-3-642-40708-6_4
Dannenberg, F., Kwiatkowska, M., Thachuk, C., Turberfield, A.J.: DNA walker circuits: computational potential, design, and verification. In: Soloveichik, D., Yurke, B. (eds.) DNA 2013. LNCS, vol. 8141, pp. 31–45. Springer, Cham (2013b). https://doi.org/10.1007/978-3-319-01928-4_3
Gray, J.N.: Notes on data base operating systems. In: Bayer, R., Graham, R.M., Seegmüller, G. (eds.) Operating Systems. LNCS, vol. 60, pp. 393–481. Springer, Heidelberg (1978). https://doi.org/10.1007/3-540-08755-9_9
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)
Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM (JACM) 37(3), 549–587 (1990)
Halpern, J.Y., Tuttle, M.R.: Knowledge, probability, and adversaries. J. ACM (JACM) 40(4), 917–960 (1993)
Hao, S.: The operation research of CDA based on PBN flight procedure. Civil Aviation Flight University of China (2012)
Henzinger, T.A., Nicollin, X., Sifakis, J.: Symbolic model checking for real-time systems. In: Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, LICS 1992, pp. 394–406. IEEE (1992)
Huth, M., Ryan, M.: Logic in computer science modelling and reasoning about system (2007)
Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997). https://doi.org/10.1007/978-1-4612-4054-9
Kooi, B.P.: Probabilistic dynamic epistemic logic. J. Logic Lang. Inform. 12(4), 381–408 (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Zheng, G. et al. (2019). Model Checking for Turn-Based Probability Epistemic Game Structure. In: Tang, Y., Zu, Q., Rodríguez García, J. (eds) Human Centered Computing. HCC 2018. Lecture Notes in Computer Science(), vol 11354. Springer, Cham. https://doi.org/10.1007/978-3-030-15127-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-15127-0_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-15126-3
Online ISBN: 978-3-030-15127-0
eBook Packages: Computer ScienceComputer Science (R0)