CTL\(^\ast\) with graded path modalities
type: Item
instance of: scholarly article
title: CTL\(^\ast\) with graded path modalities
zbMATH Open document ID: 1407.03028
author: Benjamin Aminof
author: Aniello Murano
author: Sasha Rubin
published in: Information and Computation
publication date: 2018-09-27T00:00:00Z
full work available at URL: urn:nbn:at:at-ubtuw:3-3808
review text: The paper studies Graded CTL*, an extension of the well-known branching-time temporal logic CTL* with path quantifiers that can express the existence of $k$ different paths satisfying some linear-time temporal formula, for an arbitrary $k$. This logic truly extends CTL* as it does not preserve bisimulations anymore, hence, it is more expressive. \par The main focus of the paper is a worst-case complexity analysis of the standard decision problems of model checking and satisfiability checking for this logic. Decidability is easily obtained by noticing that -- despite a general lack of invariance under bisimulations -- the logic cannot distinguish a graph model from its tree unfolding. This forms the basis of a translation into MSO interpreted over trees which yields decidability. It does not give optimal complexity bounds, though. These are obtained using the well-established automata-theoretic approach to temporal logics. The paper introduces a specialisation of alternating tree automata whose features tightly correspond to those present in the logic. It then establishes decidability of emptiness in exponential time which, for example, yields decidability of satisfiability in doubly exponential time. \par The paper is generally well written and easy to follow. The concluding section contains some interesting remarks on open problems in this area, most notably regarding the succinctness of Graded CTL* in comparison to other logics of equal expressive power.
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03D05
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6944929
zbMATH Keywords: temporal logic
zbMATH Keywords: automata
zbMATH Keywords: satisfiability
zbMATH Keywords: model checking
zbMATH Keywords: expressiveness
MaRDI profile type: Publication
OpenAlex ID: W2799335769
cites work: What’s Decidable about Weighted Automata?
cites work: Improved model checking of hierarchical systems
cites work: Graded modalities in strategy logic
cites work: On CTL* with Graded Path Modalities
cites work: Querying Regular Graph Patterns
cites work: Global Numerical Constraints on Trees
cites work: Graded computation tree logic
cites work: The Complexity of Enriched Mu-Calculi
cites work: Answering regular path queries in expressive description logics via alternating tree-automata
cites work: A note on graded modal logic
cites work: Handbook of weighted automata
cites work: Computer Aided Verification
cites work: The Complexity of Tree Automata and Logics of Programs
cites work: Deciding full branching time logic
cites work: Reasoning with Forest Logic Programs Using Fully Enriched Automata
cites work: Enriched MU-Calculi Module Checking
cites work: Model Checking for Graded CTL
cites work: CTL Model-Checking with Graded Quantifiers
cites work: In so many possible worlds
cites work: Q3457242
cites work: Decidability of SHIQ with complex role inclusion axioms
cites work: Q4809076
cites work: An automata-theoretic approach to branching-time model checking
cites work: Church's Problem Revisited
cites work: Reasoning about graded strategy quantifiers
cites work: Additional Winning Strategies in Reachability Games*†
cites work: Counting on CTL\(^*\): On the expressive power of monadic path logic
cites work: Reasoning and Query Answering in Description Logics
cites work: Q4205072
cites work: PSpace reasoning for graded modal logics
cites work: Q2757826
cites work: Reasoning about infinite computations
cites work: Monadic second-order logic on tree-like structures
DOI: 10.1016/J.IC.2018.05.001
description: scientific article; zbMATH DE number 6944929