CTL Model-Checking with Graded Quantifiers

DOI10.1007/978-3-540-88387-6_4zbMath1183.68370OpenAlexW2061668660MaRDI QIDQ3540061

Margherita Napoli, Alessandro Ferrante

Publication date: 20 November 2008

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-88387-6_4

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Temporal logic (03B44)

Related Items

CTL\(^\ast\) with graded path modalities ⋮ Model-checking graded computation-tree logic with finite path semantics

Uses Software

• SPIN
• NuSMV
• Cadence SMV
• CESAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• In so many possible worlds
• PSPACE Reasoning for Graded Modal Logics
• Packing cycles in undirected graphs
• Complexity Results for First-Order Two-Variable Logic with Counting
• Verification: Theory and Practice