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

DOI10.1016/J.TCS.2019.09.021MaRDI QIDQ2285155zbMATHOpenAlexFDO

Authors Aniello Murano, Sasha Rubin, Loredana Sorrentino, Mimmo Parente

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

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

Recommendations

• On CTL* with Graded Path Modalities
• CTL\(^\ast\) with graded path modalities
• Extended computation tree logic
• Graded computation tree logic
• Model checking for graded CTL

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 1500644 (Why is no real title available?)
• scientific article; zbMATH DE number 1500666 (Why is no real title available?)
• scientific article; zbMATH DE number 2090317 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• An automata-theoretic approach to branching-time model checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CTL Model-Checking with Graded Quantifiers
• CTL\(^\ast\) with graded path modalities
• Enriched MU-Calculi Module Checking
• Graded computation tree logic
• Graded modalities in strategy logic
• Model checking for graded CTL
• PSpace reasoning for graded modal logics
• Reasoning about graded strategy quantifiers
• Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall
• Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
• The Complexity of Enriched Mu-Calculi
• Uniform strategies, rational relations and jumping automata
• “Sometimes” and “not never” revisited

Cited in

(7)

• CTL\(^\ast\) with graded path modalities
• On CTL* with Graded Path Modalities
• Computing sufficient and necessary conditions in CTL: a forgetting approach
• Graded Computation Tree Logic with Binary Coding
• Model Checking Quantified Computation Tree Logic
• Model Checking on Trees with Path Equivalences
• CTL* model checking for data-aware dynamic systems with arithmetic

Describes a project that uses

Uses Software

• MCMAS
• MCMAS-SLK

This page was built for publication: Model-checking graded computation-tree logic with finite path semantics

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