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

DOI10.1016/J.TCS.2019.09.021zbMATH Open1436.68197OpenAlexW2974614356MaRDI QIDQ2285155FDOQ2285155

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Enriched MU-Calculi Module Checking
• PSpace reasoning for graded modal logics
• Title not available (Why is that?)
• Graded modalities in strategy logic
• Title not available (Why is that?)
• CTL Model-Checking with Graded Quantifiers
• Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
• Graded computation tree logic
• Reasoning about graded strategy quantifiers
• Model checking for graded CTL
• CTL\(^\ast\) with graded path modalities
• The Complexity of Enriched Mu-Calculi
• Uniform strategies, rational relations and jumping automata
• Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall

Cited In (6)

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

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)