A temporal logic for Markov chains

ABSTRACT

Most models of agents and multi-agent systems include information about possible states of the system (that defines relations between states and their external characteristics), and information about relationships between states. Qualitative models of this kind assign no numerical measures to these relationships. At the same time, quantitative models assume that the relationships are measurable, and provide numerical information about the degrees of relations. In this paper, we explore the analogies between some qualitative and quantitative models of agents/processes, especially those between transition systems and Markovian models.

Typical analysis of Markovian models of processes refers only to the expected utility that can be obtained by the process. On the other hand, modal logic offers a systematic method of describing phenomena by combining various modal operators. Here, we try to exploit linguistic features, offered by propositional modal logic, for analysis of Markov chains and Markov decision processes. To this end, we propose Markov temporal logic - a multi-valued logic that extends the branching time logic CTL*.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002 [doi>10.1145/585265.585270]
• 2: Adnan Aziz , Vigyan Singhal , Felice Balarin, It Usually Works: The Temporal Logic of Stochastic Systems, Proceedings of the 7th International Conference on Computer Aided Verification, p.155-165, July 03-05, 1995
• 3: Richard Ernest Bellman, Dynamic Programming, Dover Publications, Incorporated, 2003
• 4: R. Bellman. A Markovian decision process. Journal of Mathematics and Mechanics, 6:679--684, 1957.
• 5: Craig Boutilier, Sequential Optimality and Coordination in Multiagent Systems, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.478-485, July 31-August 06, 1999
• 6: Luca de Alfaro , Marco Faella , Thomas A. Henzinger , Rupak Majumdar , Mariëlle Stoelinga, Model checking discounted temporal properties, Theoretical Computer Science, v.345 n.1, p.139-170, 21 November 2005 [doi>10.1016/j.tcs.2005.07.033]
• 7: Steve Easterbrook , Marsha Chechik, A framework for multi-valued reasoning over inconsistent viewpoints, Proceedings of the 23rd International Conference on Software Engineering, p.411-420, May 12-19, 2001, Toronto, Ontario, Canada
• 8: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 9: Patrice Godefroid , Michael Huth , Radha Jagadeesan, Abstraction-Based Model Checking Using Modal Transition Systems, Proceedings of the 12th International Conference on Concurrency Theory, p.426-440, August 20-25, 2001
• 10: C. M. Grinstead and J. L. Snell. Introduction to Probability. Amer Mathematical Society, 1997.
• 11: P. Hajek. Metamathematics of Fuzzy Logic. Kluwer, 1998.
• 12: J. Y. Halpern. A logical approach to reasoning about uncertainty: a tutorial. In Discourse, Interaction, and Communication, pages 141--155. Kluwer, 1998.
• 13: H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512--535, 1994.
• 14: J. Hintikka. Logic, Language Games and Information. Clarendon Press: Oxford, 1973.
• 15: W. Jamroga. Markov temporal logic. Technical Report IfI-07-11, Clausthal University of Technology, 2007.
• 16: J. G. Kemeny, L. J. Snell, and A. W. Knapp. Denumerable Markov Chains. Van Nostrand, 1966.
• 17: B. Konikowska and W. Penczek. Model checking for multi-valued CTL*. In M. Fitting and E. Orlowska, editors, Multi-Valued Logics. 1998.
• 18: Alberto Lluch-Lafuente , Ugo Montanari, Quantitative μ-calculus and CTL defined over constraint semirings, Theoretical Computer Science, v.346 n.1, p.135-160, 23 November 2005 [doi>10.1016/j.tcs.2005.08.006]
• 19: K. Lorenz and P. Lorenzen. Dialogische Logik. Darmstadt, 1978.
• 20: A. Markov. Rasprostranenie zakona bol'shih chisel na velichiny, zavisyaschie drug ot druga. Izvestiya Fiziko-matematicheskogo obschestva pri Kazanskom universitete, 2(15):135--156, 1906.
• 21: Nils J. Nilsson, Probabilistic logic, Artificial Intelligence, v.28 n.1, p.71-88, Feb. 1986 [doi>10.1016/0004-3702(86)90031-7]
• 22: Enrique H. Ruspini , John D. Lowrance , Thomas M. Strat, Understanding evidential reasoning, International Journal of Approximate Reasoning, v.6 n.3, p.401-424, May 1992 [doi>10.1016/0888-613X(92)90033-V]
• 23: L. Zadeh. Fuzzy sets. Information and Control, 8(3):338--353, 1965.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence
            Subjects: Multiagent systems

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.4 Knowledge Representation Formalisms and Methods
          Subjects: Modal logic

General Terms:
Theory

Keywords:
Markov chains, Markov decision processes, temporal logic