Logics for Markov Desicion Processes

PEDRO SÁNCHEZ TERRAF; PEDRO R. D'ARGENIO; NICOLAS WOLOVICK

Bogotá

Simposio; Simposio Latinoamericano de Lógica Matemática; 2012

Universidad de los Andes

Larsen and Skou introduced a modal logic, based on Hennessy-Milner's, to describe behavior for Probabilistic Transition Systems. Later Desharnais et al. proved that already a fragment of that logic is complete for bisimilarity on the broad class of labelled Markov processes (LMP) over analytic spaces, whereas Larsen & Skou only considered discrete systems. We extended the LMP model with non-determinism and studied bisimulations. We developed a logic complete for bisimilarity over analytic spaces under the assumption of image-finiteness. In this talk I'll survey these results, some (counter)examples and open problems concerning the new model and its logic. Joint work with Pedro D'Argenio and Nicolás Wolovick.