Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall

DOI10.1007/978-3-642-02734-5_8MaRDI QIDQ3393383zbMATH OpenOpenAlexFDO

Authors Cătălin Dima

Publication date 20 August 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02734-5_8

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) Agent technology and artificial intelligence (68T42)

Recommendations

• scientific article; zbMATH DE number 1500666
• Well-structured model checking of multiagent systems
• scientific article; zbMATH DE number 5051662
• Model Checking Knowledge and Linear Time: PSPACE Cases
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

Cites work

• An Introduction to Symbolic Dynamics and Coding
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• Common knowledge and update in finite environments
• Decidability and undecidability of extensions of second (first) order theory of (generalized) successor
• scientific article; zbMATH DE number 1500666 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 1405651 (Why is no real title available?)
• scientific article; zbMATH DE number 5051652 (Why is no real title available?)
• Infinite trees and automaton-definable relations over -words
• The complexity of reasoning about knowledge and time. I: Lower bounds
• The tree of knowledge in action: towards a common perspective

Cited in

(6)

• Model-checking graded computation-tree logic with finite path semantics
• Uniform strategies, rational relations and jumping automata
• scientific article; zbMATH DE number 1500666 (Why is no real title available?)
• Synchronous or alternating? LTL black-box checking of Mealy machines by combining the LearnLib and LTSmin
• The complexity of second-order HyperLTL
• The complexity of second-order HyperLTL

Describes a project that uses

Uses Software

• MONA

This page was built for publication: Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall

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