Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Model Checking for Turn-Based Probability Epistemic Game Structure

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNISA,volume 11354))

Included in the following conference series:

  • 1223Accesses

Abstract

In this paper, aturn-based probability epistemic game structure (TPEGS) is proposed to model knowledge preconditions for actions of system and environment firstly, which is an extension ofturn-based synchronous game structures with probabilistic transition. Secondly, we introduce probability operator\( P_{\sim \lambda } \) intoalternating temporal epistemic logic (ATEL) and defineturn-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

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide -see info

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)

    Google Scholar 

  • Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput.104(1), 2–34 (1993)

    Article MathSciNet  Google Scholar 

  • Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM (JACM)49(5), 672–713 (2002)

    Article MathSciNet  Google Scholar 

  • 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

    Chapter  Google Scholar 

  • 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

    Chapter MATH  Google Scholar 

  • 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)

    Google Scholar 

  • 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

    Chapter  Google Scholar 

  • Dowek, G., Munoz, C., Carreno, V.A.: Abstract model of the SATS concept of operations: initial results and recommendations (2004)

    Google Scholar 

  • Fagin, R., Halpern, J.Y., Megiddo, N.: A logic for reasoning about probabilities. Inf. Comput.87(1), 78–128 (1990)

    Article MathSciNet  Google Scholar 

  • 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

    Chapter  Google Scholar 

  • 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

    Chapter MATH  Google Scholar 

  • 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

    Chapter  Google Scholar 

  • Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput.6(5), 512–535 (1994)

    Article  Google Scholar 

  • Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM (JACM)37(3), 549–587 (1990)

    Article MathSciNet  Google Scholar 

  • Halpern, J.Y., Tuttle, M.R.: Knowledge, probability, and adversaries. J. ACM (JACM)40(4), 917–960 (1993)

    Article MathSciNet  Google Scholar 

  • Hao, S.: The operation research of CDA based on PBN flight procedure. Civil Aviation Flight University of China (2012)

    Google Scholar 

  • 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)

    Google Scholar 

  • Huth, M., Ryan, M.: Logic in computer science modelling and reasoning about system (2007)

    Google Scholar 

  • Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997).https://doi.org/10.1007/978-1-4612-4054-9

    Book MATH  Google Scholar 

  • Kooi, B.P.: Probabilistic dynamic epistemic logic. J. Logic Lang. Inform.12(4), 381–408 (2003)

    Article MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Systems Engineering Research Institute, Beijing, China

    Guocheng Zheng, Pin Wang, Xinyu Zhang, Chuan Zhang & Mengao Li

  2. North China Electric Power University, Baoding, 071003, China

    Yuxiao Yang & Weifeng Xu

Authors
  1. Guocheng Zheng

    You can also search for this author inPubMed Google Scholar

  2. Pin Wang

    You can also search for this author inPubMed Google Scholar

  3. Xinyu Zhang

    You can also search for this author inPubMed Google Scholar

  4. Chuan Zhang

    You can also search for this author inPubMed Google Scholar

  5. Mengao Li

    You can also search for this author inPubMed Google Scholar

  6. Yuxiao Yang

    You can also search for this author inPubMed Google Scholar

  7. Weifeng Xu

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence toWeifeng Xu.

Editor information

Editors and Affiliations

  1. South China Normal University, Guangzhou, China

    Yong Tang

  2. Wuhan University of Technology, Wuhan City, China

    Qiaohong Zu

  3. CINVESTAV, Mexico City, Mexico

    José G. Rodríguez García

Rights and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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

Publish with us

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide -see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

[8]ページ先頭
©2009-2025 Movatter.jp