A Temporal Logic for Stochastic Multi-Agent Systems

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 characterizing processes by combining various modal operators. A multivalued temporal logic for Markov chains and Markov decision processes has been recently proposed in [1]. Here, we discuss how it can be extended to the mufti-agent case. We relate the resulting logic to existing (two-valued) logics of strategic ability, and present fixpoint characterizations for some natural combinations of strategic and temporal operators.