Skip Navigation



Journal of Logic and Computation Advance Access published online on May 4, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp027
This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Rybakov, V.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Linear Temporal Logic LTLK extended by Multi-Agent Logic Kn with Interacting Agents

Vladimir Rybakov

Department of Computing and Mathematics, Manchester Metropolitan University, Manchester M1 5GD, UK and Siberian Federal University, Krasnoyarsk, Russia.
E-mail: v.rybakov{at}mmu.ac.uk

Received 13 June 2008.

We study an extension LTLK of the linear temporal logic LTLK by implementing multi-agent knowledge logic KD45m (which is often referred as multi-modal logic S5m). The temporal language of our logic adapts the operations U (until) and N (next) and uses new temporal operations: Uw—weak until, and Us—strong until. We also employ the standard agents’ knowledge operations Ki from the multi-agent logic KD45m and extend them with an operation IntK responsible for knowledge obtained via interaction of agents. The semantic models for LTLK are Kripke/Hintikka-like structures NC based on the linear time. Structures NC use i isin N as indexes for time, and the base set of any NC consists of clusters C(i) (for all i isin N) containing all possible states at the time i. Agents’ knowledge is modelled in time clusters C(i) via agents’ knowledge accessibility relations Rj. The logic LTLK is the set of all formulas which are valid (true) in all such models NC w.r.t. all possible valuations. We prove that LTLK is decidable: we reduce the decidability problem to verification of validity for special normal reduced forms of rules in specific models (not LTLK models) of size single-exponential in size of the rules. Furthermore, we extend these results to a linear temporal logic LTLK(Z) based on the time flow indexed by all integer numbers (with additional operations Since and Previous). Also we show that LTLK has the finite model property (fmp) while LTLK (Z) has no standard fmp.

Keywords: Linear temporal logic; modal logics multi-agent logic; interacting agents; decidability; algorithms; inference rules



References

  1. Barringer H, Fisher N, Gabbay D, Gough. G. Advances in temporal logic. (1999) Kluwer Academic Publishers. Vol. 16 of Applied logic series.
  2. Braüner. T. Natural deduction for hybrid logic. Journal of Logic and Computation (2004) 14:329–353.[Abstract/Free Full Text]
  3. Braüner T. T. Two natural deduction systems for hybrid logic. Journal of Logic, Language and Computation (2004) 13:1–23.[CrossRef]
  4. Baader F, Calvanese D, McGuinness DL, Nardi D, Patel-Schneider P, eds. The Description Logic Handbook, Implementations and Applications (2003) Cambridge University Press.
  5. Blackburn P, Marx. M. Constructive interpolation in hybrid logic. Journal of Symbolic Logic (2003) 68:463–480.[CrossRef][Web of Science]
  6. Areces C, Blackburn P, Marx. M. Hybrid logic: characterization, interpolation and complexity. Journal of Symbolic Logic (2001) 66:977–1010.[CrossRef][Web of Science]
  7. Bull. RA. An algebraic study of tense logics with linear time. The Journal of Symbolic Logic (1968) 33:27–38.[CrossRef]
  8. Bull. RA. Note on a paper in tense logic. The Journal of Symbolic Logic (1969) 34:215–218.[CrossRef]
  9. Clarke E, Grumberg O, Hamaguchi. KP. Another look at LTL model checking. (1994) Springer. In Conference on Computer Aided Verification (CAV), Stanford, California, 1994. Vol. 818 of Lecture Notes in Computer Science.
  10. Daniele M, Giunchiglia F, Vardi. M. Improved automata generation for linear temporal logic. (1999) In (CAV’99), International Conference on Computer-Aided Verification, Trento, Italy.
  11. Emerson. EA. Temporal and modal logics. In: Handbook of Theoretical Computer Science—van Leenwen J, ed. (1990) Elsevier Science. 996–1072.
  12. Fagin R, Halpern J, Moses Y, Vardi. M. Reasoning About Knowledge (1995) The MIT Press.
  13. Fagin J, Geanakoplos E, Halpern J, Vardi. M. The hierarchical approach to modeling knowledge and common knowledge. International Journal of Game Theory (1999) 28:331–365.[CrossRef][Web of Science]
  14. Governatori G, Orgun AM, Liu. C. Modal tableaux for verifying stream authentication protocols. Journal of Autonomous Agents and Multi Agent Systems (2008) (forthcoming).
  15. Gabbay D, Queiroz. Rde. The functional interpretation of modal necessity. In: Advancies in Intensional Logic—de Rijke, ed. (1997) Kluwer. 59–91.
  16. Gabbay D, Pnueli A, Shelah S, Stavi. J. On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1980) ACM Press. 163–173.
  17. Gabbay DM, Hodkinson. IM. An axiomatisation of the temporal logic with Until and Since over the real numbers. Journal of Logic and Computation (1990) 1:229–260.[Abstract/Free Full Text]
  18. Goldblatt. R. Logics of Time and Computation. CSLI Lecture Notes (1992) 7.
  19. Halpern J, Shore. R. Reasoning about common knowledge with infinitely many agents. Information and Computation (2004) 191:1–40.[CrossRef][Web of Science]
  20. Halpern J, van der Meyden R, Vardi. M. Complete axiomatizations for reasoning about knowledge and time. SIAM Journal on Computing (2004) 33:674–703.[CrossRef][Web of Science]
  21. Hammer M, Knapp A, Merz. St. Truly On-the-Fly LTL Model Checking. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) (2005) 191–205.
  22. Hodkinson. I. Temporal logic and automata. In: Temporal Logic: Mathematical Foundations and Computational Aspects—Gabbay DM, Reynolds MA, Finger M, eds. (2000) 2. Clarendon Press. 30–72. ChII.
  23. Kroger F, Merz. St. Temporal Logic and State Systems (2008) Springer.
  24. Manna Z, Pnueli. A. TheTemporal Logic of Reactive and Concurrent Systems: Specification (1992) Springer.
  25. Manna Z, Pnueli. A. Temporal Verification of Reactive Systems: Safety (1995) Springer.
  26. Penczek W, Lomusico. A. Verifying epistemic properties of milti-agent systemse via bounded model checking. Fundamenta Informaticae (2003) 55:167–185.[Web of Science]
  27. Pnueli. A. The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science (1977) IEEE. 46–57.
  28. Prior. A. The Past Present and Future (1967) Oxford University Press.
  29. Prior. A. Papers on Time and Tense (2003) new edn. Oxford University Press.
  30. Rao AS, Georgeff. MP. Decision procedures for BDI logics. Journal of Logic and Computation (1998) 8:293–343.[Abstract/Free Full Text]
  31. Rybakov. VV. Rules of inference with parameters for intuitionistic logic. Journal of Symbolic Logic (1992) 57:912–923.[CrossRef][Web of Science]
  32. Rybakov. VV. Hereditarily structurally complete modal logics. Journal of Symbolic Logic (1995) 60:266–288.[CrossRef][Web of Science]
  33. Rybakov. VV. Admissible logical inference rules. In: Studies in Logic and the Foundation of Mathematics, vol. 136 (1997) Elsevier.
  34. Rybakov VV, Kiyatkin VR, Oner. T. On finite model property for admissible rules. Mathematical Logic Quarterly (1999) 45:505–520.[Web of Science]
  35. Rybakov. VV. Construction of an explicit basis for rules admissible in modal system S4. Mathematical Logic Quarterly (2001) 47:441–451.[CrossRef][Web of Science]
  36. Rybakov. VV. Logical consecutions in discrete linear temporal logic. Journal of Symbolic Logic (2005) 70:1137–1149.[CrossRef][Web of Science]
  37. Rybakov. VV. Logical consecutions in intransitive temporal linear logic of finite intervals. Journal of Logic Computation (2005) 15:633–657.
  38. Rybakov. VV. Linear temporal logic with Until and Before on integer numbers, deciding algorithms. In: Computer Science–Theory and Applications (2006) Springer. 322–334. Vol. 3967 of Lecture Notes in Computer Science.
  39. Rybakov. V. Since-until temporal logic based on parallel time with common past. In: Logical Foundation of Computer Science (2007) Springer. 486–497. Vol. 4514 of Lecture Notes in Computer Science.
  40. Rybakov. V. Logic of discovery in uncertain situations–decciding algorithms. In: Knowledge-Based and Intelligent Information & Engineering Systems 2007 (2007) Springer: Vetri sul Mare. 950–968. Vol. 4694 of Lecture Notes in Artificial Intelligence.
  41. Vardi. M. An automata-theoretic approach to linear temporal logic. In: Proceedings of the Banff Workshop on Knowledge Acquisition (Banff’94) (1994).
  42. van Benthem. J. The Logic of Time (1991) Kluwer.
  43. van Benthem J, Bergstra. JA. Logic of transition systems. Journal of Logic, Language and Information (1994) 3:247–283.[CrossRef]
  44. van der Hoek W, Wooldridge. M. Model checking knowledge and time. In: 9thWorshop on SPIN (Model Checking Software) (2002) Grenoble.
  45. van der Meyden R, Shilov. NN. Model checking knowledge and time in systems with perfect recall. (1999) Springer. 432–445. Vol. 1738 of Lecture Notes in Computer Science.

Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Rybakov, V.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?