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

DOI10.1007/978-3-642-02734-5_8zbMath1250.03026OpenAlexW2214827277MaRDI QIDQ3393383

Catalin 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) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Agent technology and artificial intelligence (68T42)

Related Items (2)

Model-checking graded computation-tree logic with finite path semantics ⋮ Uniform strategies, rational relations and jumping automata

Uses Software

• MONA

Cites Work

• The complexity of reasoning about knowledge and time. I: Lower bounds
• Infinite trees and automaton-definable relations over \(\omega\)-words
• Common knowledge and update in finite environments
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• An Introduction to Symbolic Dynamics and Coding
• Decidability and undecidability of extensions of second (first) order theory of (generalized) successor
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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