Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Exponential improvement of time complexity of model checking for multiagent systems with perfect recall

  • Published:
Programming and Computer Software Aims and scope Submit manuscript

Abstract

The model checking algorithm for a combination of the computation tree logic (CTL) and the propositional logic of knowledge (PLK) in multiagent systems with perfect recall is revised. The proposed approach is based on data structures that are exponentially smaller than the structures used in the previous version of this checking algorithm. Thus, the time complexity of this algorithm is exponentially reduced.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Abdulla, P.A., Ĉerâns, K., Jonsson, B., and Tsay Yih-Kuen, Algorithmic Analysis of Programs with Well Quasi-Ordered Domains, Inf. Comput., 2000, vol. 160, no. 1/2, pp. 109–127.

    Article  MATH  Google Scholar 

  2. Bordini, R.H., Fisher, M., Visser, W., and Wooldridge, M., Verifying Multi-Agent Programs by Model Checking, Autonomous Agents Multi-Agent Syst., 2006, vol 12, no. 2, pp. 239–256.

    Article  Google Scholar 

  3. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., and Hwang, L.J., Symbolic Model Checking: 1020 States and Beyond, Inf. Comput., 1992, vol. 98, no. 2, pp. 142–170.

    Article  MathSciNet  MATH  Google Scholar 

  4. Clarke, E.M., Grumberg, O., and Peled D., Model Checking, Cambridge, Mass.: MIT Press, 1999.

    Google Scholar 

  5. Cohen, M. and Lomuscio, A., Non-elementary Speed up for Model Checking Synchronous Perfect Recall, Proc. of the 2010 Conf. on ECAI 2010, Amsterdam: IOS Press, 2010, pp. 1077–1078.

    Google Scholar 

  6. Emerson, E.A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, van Leeuwen, J., Ed., Amsterdam: Elsevier; Cambridge, Mass.: MIT Press, 1990, pp. 995–1072.

    Google Scholar 

  7. Fagin, R., Halpern, J.Y., Moses, Y., and Vardi, M.Y., Reasoning about Knowledge, Cambridge, Mass.: MIT Press, 1995.

    MATH  Google Scholar 

  8. Finkel, A. and Schnoebelen, Ph. Well-structured Transition Systems Everywhere! Theor. Comput. Sci., 2001, vol. 256, nos. 1–2, pp. 63–92.

    Article  MathSciNet  MATH  Google Scholar 

  9. Garanina, N.O., Kalinina, N.A., and Shilov N.V., Model Checking Knowledge, Actions and Fixpoints, Proc. of Concurrency, Specification and Programming Workshop CS&P’2004, Germany, 2004, Berlin: Humboldt Universitat, Informatik-Bericht, 2004, vol. 2, no. 170, pp. 351–357.

    Google Scholar 

  10. Halpern, J.Y., van der Meyden, R., and Vardi, M.Y., Complete Axiomatizations for Reasoning about Knowledge and Time, SIAM J. Comput., 2004, vol. 33, no. 3, pp. 674–703.

    Article  MathSciNet  MATH  Google Scholar 

  11. Huang, X. and van der Meyden, R., The Complexity of Epistemic Model Checking: Clock Semantics and Branching Time, Proc. of the 19th ECAI, Lisbon; in Frontiers in Artificial Intelligence and Applications, Amsterdam: IOS, 2010, vol. 215, pp. 549–554.

    Google Scholar 

  12. Kozen, D., Results on the Propositional Mu-Calculus, Theor. Comput. Sc., 1983, vol. 27, no. 3, pp. 333–354.

    Article  MathSciNet  MATH  Google Scholar 

  13. Kozen, D. and Tiuryn, J., Logics of Programs, in Handbook of Theoretical Computer Science, van Leeuwen, J., Ed., Amsterdam: Elsevier, 1990, pp. 789–840.

    Google Scholar 

  14. Kwiatkowska, M.Z., Lomuscio, A., and Qu, H., Parallel Model Checking for Temporal Epistemic Logic, Proc. of the 19th ECAI, Lisbon; in Frontiers in Artificial Intelligence and Applications, Amsterdam: IOS Press, 2010, vol. 215, pp. 543–548.

    Google Scholar 

  15. Lomuscio, A., Penczek, W., and Qu, H., Partial Order Reductions for Model Checking Temporal Epistemic Logics over Interleaved Multi-Agent Systems, Proc. of the 9th AAMAS, Toronto, 2010, IFAAMAS, 2010, vol. 1, pp. 659–666.

    Google Scholar 

  16. Van der Meyden R. and Shilov, N.V., Model Checking Knowledge and Time in Systems with Perfect Recall, Lect. Notes Comput. Sci., 1999, vol. 1738, pp. 432–445.

    Article  Google Scholar 

  17. Rescher, N., Epistemic Logic. A Survey of the Logic of Knowledge, Pitsburgh: University of Pitsburgh Press, 2005.

    Google Scholar 

  18. Shilov, N.V. and Yi, K., How to Find a Coin: Propositional Program Logics Made Easy, in Current Trends in Theoretical Computer Science, World Scientific, 2004, vol. 2, pp. 181–213.

    Google Scholar 

  19. Shilov, N.V., Garanina, N.O., and Choe, K.-M., Update and Abstraction in Model Checking of Knowledge and Branching Time, Fundameta Informaticae, 2006, vol. 72, nos. 1–3, pp. 347–361.

    MathSciNet  MATH  Google Scholar 

  20. Shilov, N.V. and Garanina, N.O., Well-Structured Model Checking of Multiagent Systems, Proc. of the 6th Int. Conf. on Perspectives of System Informatics, Novosibirsk, 2006, Lect. Notes in Comput. Sci., 2006, vol. 4378.

Download references

Author information

Authors and Affiliations

  1. Ershov Institute of Information Systems, Siberian Branch, Russian Academy of Sciences, pr. Akademika Lavrent’eva 6, Novosibirsk, 630090, Russia

    N. O. Garanina

Authors
  1. N. O. Garanina
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to N. O. Garanina.

Additional information

Original Russian Text © N.O. Garanina, 2012, published in Programmirovanie, 2012, Vol. 38, No. 6.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Garanina, N.O. Exponential improvement of time complexity of model checking for multiagent systems with perfect recall. Program Comput Soft 38, 294–303 (2012). https://doi.org/10.1134/S0361768812060047

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1134/S0361768812060047

Keywords

Search

Navigation