Model-checking graded computation-tree logic with finite path semantics
From MaRDI portal
Publication:2285155
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
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
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