Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

DOI10.1145/3409250MaRDI QIDQ5034220zbMATH OpenOpenAlexWikidataFDO

Authors Ron van der Meyden, Manas K. Patra

Publication date 24 February 2022

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1511.03003

zbMATH Keywords

decidabilitylogic of knowledgelogic of probabilitymodel checkingpartially observable Markov chains

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We investigate the decidability of model-checking logics of time, knowledge and probability, with respect to two epistemic semantics: the clock and synchronous perfect recall semantics in partially observed discrete-time Markov chains. Decidability results are known for certain restricted logics with respect to these semantics, subject to a variety of restrictions that are either unexplained or involve a longstanding unsolved mathematical problem. We show that mild generalizations of the known decidable cases suffice to render the model checking problem definitively undecidable. In particular, for a synchronous perfect recall, a generalization from temporal operators with finite reach to operators with infinite reach renders model checking undecidable. The case of the clock semantics is closely related to a monadic second order logic of time and probability that is known to be decidable, except on a set of measure zero. We show that two distinct extensions of this logic make model checking undecidable. One of these involves polynomial combinations of probability terms, the other involves monadic second order quantification into the scope of probability operators. These results explain some of the restrictions in previous work.

Recommendations

• Undecidable cases of model checking probabilistic temporal-epistemic logic (extended abstract)
• scientific article; zbMATH DE number 2182497
• On undecidability of propositional temporal logics on trace systems
• Probabilistic Temporal Logics
• A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic
• Probabilistic propositional temporal logics
• A decidable probability logic for timed probabilistic systems
• Probabilistic temporal logics via the modal mu-calculus

Cited in

(9)

• The complexity of epistemic model checking: clock semantics and branching time
• Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall
• The tree of knowledge in action: towards a common perspective
• Explicit and implicit indeterminism reasoning about uncertain and contradictory specifications of dynamic systems
• scientific article; zbMATH DE number 2182497 (Why is no real title available?)
• Separable GPL: decidable model checking with more non-determinism
• Undecidable cases of model checking probabilistic temporal-epistemic logic (extended abstract)
• Synchronizing diachronic uncertainty
• A probabilistic temporal epistemic logic: decidability

This page was built for publication: Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5034220)