Model-checking graded computation-tree logic with finite path semantics

DOI10.1016/j.tcs.2019.09.021zbMath1436.68197OpenAlexW2974614356MaRDI QIDQ2285155

Sasha Rubin, Loredana Sorrentino, Aniello Murano

Publication date: 16 January 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2019.09.021

zbMATH Keywords

model checkingcomputation tree logicfinite paths

Mathematics Subject Classification ID

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

Computing sufficient and necessary conditions in CTL: a forgetting approach ⋮ CTL* model checking for data-aware dynamic systems with arithmetic

Uses Software

• MCMAS
• MCMAS-SLK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Graded modalities in strategy logic
• Reasoning about graded strategy quantifiers
• CTL\(^\ast\) with graded path modalities
• Uniform strategies, rational relations and jumping automata
• PSPACE Reasoning for Graded Modal Logics
• Graded computation tree logic
• Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall
• Model Checking for Graded CTL
• Enriched MU-Calculi Module Checking
• The Complexity of Enriched Mu-Calculi
• CTL Model-Checking with Graded Quantifiers
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• “Sometimes” and “not never” revisited
• An automata-theoretic approach to branching-time model checking
• Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies