Model checking for epistemic and temporal properties of uncertain agents

Abstract

In this paper, we introduce a probabilistic epistemic temporal logic, called PETL, which is a combination of temporal logic and probabilistic knowledge logic. The model checking algorithm is given. Furthermore, we present a probabilistic epistemic temporal logic, called μPETL, which generalizes μ-calculus by adding probabilistic knowledge modality. Similar to μ-calculus, μ.PETL is a succinct and expressive language. It is showed that temporal modalities such as "always", "sometime" and "until", and probabilistic knowledge modalities such as "probabilistic knowledge" and "probabilistic common knowledge" can be expressed in such a logic. PETL is proven to be a sublogic of μPETL. The model checking technique for μ.PETL is also studied. © Springer-Verlag Berlin Heidelberg 2006.