Undecidable cases of model checking probabilistic temporal-epistemic logic (extended abstract)

zbMATH Open1483.68210arXiv1606.08815MaRDI QIDQ5015397FDOQ5015397

Authors: Ron van der Meyden, Manas K. Patra 

Publication date: 7 December 2021

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

Recommendations

• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
• scientific article; zbMATH DE number 1948170
• scientific article; zbMATH DE number 1500666
• A Logic of Probability with Decidable Model Checking
• A decidable probability logic for timed probabilistic systems

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• VERICS 2007 -- a model checker for knowledgee and real-time
• Title not available (Why is that?)
• Communication Theory of Secrecy Systems*
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Title not available (Why is that?)
• Reasoning about knowledge and probability
• Title not available (Why is that?)
• A logic for reasoning about probabilities
• Weak Second‐Order Arithmetic and Finite Automata
• The complexity of epistemic model checking: clock semantics and branching time
• Computer Aided Verification
• Positivity Problems for Low-Order Linear Recurrence Sequences
• Title not available (Why is that?)
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• A Logic of Probability with Decidable Model Checking
• Title not available (Why is that?)
• Reachability problems for Markov chains
• Title not available (Why is that?)
• Complete axiomatizations for reasoning about knowledge and branching time
• Model Checking Knowledge and Linear Time: PSPACE Cases
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors

Cited In (3)

• Title not available (Why is that?)
• The complexity of epistemic model checking: clock semantics and branching time
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

Uses Software

• VerICS
• MCMAS
• MCK

This page was built for publication: Undecidable cases of model checking probabilistic temporal-epistemic logic (extended abstract)

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