research-article

A temporal logic for Markov chains

Author:

Wojciech JamrogaAuthors Info & Claims

AAMAS '08: Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 2

Pages 697 - 704

Published: 12 May 2008 Publication History

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]

R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672--713, 2002.

Digital Library

[2]

A. Aziz, V. Singhal, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. It usually works: The temporal logic of stochastic systems. In Proceedings of CAV, volume 939 of LNCS, pages 155--165, 1995.

[3]

R. Bellman. Dynamic Programming. Princeton University Press, 1957.

Digital Library

[4]

R. Bellman. A Markovian decision process. Journal of Mathematics and Mechanics, 6:679--684, 1957.

[5]

C. Boutilier. Sequential optimality and coordination in multiagent systems. In Proceedings of IJCAI, pages 478--485, 1999.

Digital Library

[6]

L. de Alfaro, M. Faella, T. Henzinger, R. Majumdar, and M. Stoelinga. Model checking discounted temporal properties. Theoretical Computer Science, 345:139--170, 2005.

Digital Library

[7]

S. Easterbrook and M. Chechik. A framework for multi-valued reasoning over inconsistent viewpoints. In International Conference on Software Engineering, pages 411--420, 2001.

Digital Library

[8]

E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, pages 995--1072. Elsevier Science Publishers, 1990.

Digital Library

[9]

P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based model checking using modal transition systems. In Proceedings of CONCUR, volume 2154 of LNCS, pages 426--440, 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.

Digital Library

[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]

A. Lluch-Lafuente and U. Montanari. Quantitative μ-calculus and CTL based on constraint semirings. Electr. Notes Theor. Comput. Sci., 112:37--59, 2005.

Digital Library

[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]

N. J. Nilsson. Probabilistic logic. Artificial Intelligence, 28(1):71--87, 1986.

Digital Library

[22]

E. Ruspini, J. Lowrance, and T. Strat. Understanding evidential reasoning. Artificial Intelligence, 6(3):401--424, 1992.

Digital Library

[23]

L. Zadeh. Fuzzy sets. Information and Control, 8(3):338--353, 1965.

Cited By

Jamroga WKonikowska BPenczek WJonker CMarsella SThangarajah JTuyls K(2016)Multi-Valued Verification of Strategic AbilityProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937097(1180-1189)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937097
Wan WBentahar JYahyaoui HBen Hamza A(2016)Verifying concurrent probabilistic systems using probabilistic-epistemic logic specificationsApplied Intelligence10.1007/s10489-016-0790-245:3(747-776)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1007/s10489-016-0790-2
Broersen J(2013)Probabilistic stit logic and its decompositionInternational Journal of Approximate Reasoning10.1016/j.ijar.2012.08.00754:4(467-477)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1016/j.ijar.2012.08.007
Show More Cited By

Index Terms

A temporal logic for Markov chains
1. Computing methodologies
  1. Artificial intelligence
    1. Distributed artificial intelligence
      1. Multi-agent systems
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Markov Chains and Markov Decision Processes in Isabelle/HOL

This paper presents an extensive formalization of Markov chains (MCs) and Markov decision processes (MDPs), with discrete time and (possibly infinite) discrete state-spaces. The formalization takes a coalgebraic view on the transition systems ...
A complete proof system for propositional projection temporal logic

The paper presents a proof system for Propositional Projection Temporal Logic (PPTL) with projection-plus. The syntax, semantics, and logical laws of PPTL are introduced together with an axiom system consisting of axioms and inference rules. To ...
On temporal logic versus datalog
Logic and complexity in computer science

We provide a direct and modular translation from the temporal logics CTL, ETL, FCTL (CTL extended with the ability to express fairness) and the Modal µ-calculus to Monadic inf-Datalog with built-in predicates. We call it inf-Datalog because the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

AAMAS '08: Proceedings of the 7th international joint conference on Autonomous agents and multiagent systems - Volume 2

May 2008

673 pages

ISBN:9780981738116

Sponsors

ACM: Association for Computing Machinery
AAAI: Association for the Advancement of Artifical Intelligence

In-Cooperation

SIGAI: ACM Special Interest Group on Artificial Intelligence

Publisher

International Foundation for Autonomous Agents and Multiagent Systems

Richland, SC

Publication History

Published: 12 May 2008

Check for updates

Author Tags

Qualifiers

Research-article

Conference

AAMAS08

Sponsor:

ACM
AAAI

AAMAS08: 7th International Conference on Autonomous Agents and Multi Agent Systems

May 12 - 16, 2008

Estoril, Portugal

Acceptance Rates

Overall Acceptance Rate 1,155 of 5,036 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
333
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 29 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jamroga WKonikowska BPenczek WJonker CMarsella SThangarajah JTuyls K(2016)Multi-Valued Verification of Strategic AbilityProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937097(1180-1189)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937097
Wan WBentahar JYahyaoui HBen Hamza A(2016)Verifying concurrent probabilistic systems using probabilistic-epistemic logic specificationsApplied Intelligence10.1007/s10489-016-0790-245:3(747-776)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1007/s10489-016-0790-2
Broersen J(2013)Probabilistic stit logic and its decompositionInternational Journal of Approximate Reasoning10.1016/j.ijar.2012.08.00754:4(467-477)Online publication date: 1-Jun-2013
https://dl.acm.org/doi/10.1016/j.ijar.2012.08.007
van der Hoek WWooldridge M(2012)Logics for Multiagent SystemsAI Magazine10.1609/aimag.v33i3.242733:3(92-105)Online publication date: 1-Sep-2012
https://dl.acm.org/doi/10.1609/aimag.v33i3.2427
Broersen J(2011)Probabilistic stit logicProceedings of the 11th European conference on Symbolic and quantitative approaches to reasoning with uncertainty10.5555/2026067.2026118(521-531)Online publication date: 29-Jun-2011
https://dl.acm.org/doi/10.5555/2026067.2026118
Wan WBentahar JHamza A(2011)Model checking epistemic and probabilistic properties of multi-agent systemsProceedings of the 24th international conference on Industrial engineering and other applications of applied intelligent systems conference on Modern approaches in applied intelligence - Volume Part II10.5555/2025816.2025824(68-78)Online publication date: 28-Jun-2011
https://dl.acm.org/doi/10.5555/2025816.2025824

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents