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

MaRDI QIDQ5015397zbMATH OpenFDO

Authors Ron van der Meyden, Manas K. Patra

Publication date 7 December 2021

Full work available at URL https://arxiv.org/abs/1606.08815, http://eptcs.web.cse.unsw.edu.au/paper.cgi?TARK2015.19

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)

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

Cites work

• scientific article; zbMATH DE number 3823893 (Why is no real title available?)
• scientific article; zbMATH DE number 140397 (Why is no real title available?)
• scientific article; zbMATH DE number 3543391 (Why is no real title available?)
• scientific article; zbMATH DE number 545277 (Why is no real title available?)
• scientific article; zbMATH DE number 1973372 (Why is no real title available?)
• scientific article; zbMATH DE number 2046116 (Why is no real title available?)
• scientific article; zbMATH DE number 1500666 (Why is no real title available?)
• scientific article; zbMATH DE number 3371972 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• A Logic of Probability with Decidable Model Checking
• A logic for reasoning about probabilities
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• Communication Theory of Secrecy Systems*
• Complete axiomatizations for reasoning about knowledge and branching time
• Computer Aided Verification
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
• Model Checking Knowledge and Linear Time: PSPACE Cases
• Positivity problems for low-order linear recurrence sequences
• Reachability problems for Markov chains
• Reasoning about knowledge and probability
• The complexity of epistemic model checking: clock semantics and branching time
• VERICS 2007 -- a model checker for knowledgee and real-time
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(4)

• scientific article; zbMATH DE number 2182497 (Why is no real title available?)
• A probabilistic temporal epistemic logic: decidability
• The complexity of epistemic model checking: clock semantics and branching time
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

Describes a project that uses

Uses Software

• MCK
• MCMAS
• VerICS

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)