Go to page
 

Bibliographic Metadata

Title
On CTL with Graded Path Modalities
AuthorAminof, Benjamin ; Murano, Aniello ; Rubin, Sasha
Published in
Logic for Programming, Artificial Intelligence, and Reasoning. 20th International Conference, LPAR-20 2015 : Davis, Martin; Fehnker, Ansgar; McIver, Annabelle; Voronkov, Andrei, Fiji Islands, 2015, page 281-296
Published2015
LanguageEnglish
SeriesLecture Notes in Computer Science ; 9450
Document typeArticle in a collected edition
Project-/ReportnumberAustrian Science Fund (FWF): S11403-N23 (RiSE)
Project-/ReportnumberVienna Science and Technology Fund (WWTF): ICT12-059
Project-/ReportnumberEuropean Union's FP7: 600958-SHERPA
ISBN9783662488997
URNurn:nbn:at:at-ubtuw:3-3808 Persistent Identifier (URN)
DOI10.1007/978-3-662-48899-7_20 
Restriction-Information
 The work is publicly available
Files
On CTL with Graded Path Modalities [0.4 mb]
Links
Reference
Classification
Abstract (English)

Graded path modalities count the number of paths satisfying a property, and generalize the existential (E) and universal (A) path modalities of CTL. The resulting logic is denoted GCTL, and is a very powerful logic since (as we show) it is equivalent, over trees, to monadic path logic. We settle the complexity of the satisfiability problem of GCTL, i.e., 2ExpTime-Complete, and the complexity of the model checking problem of GCTL, i.e., PSpace-Complete. The lower bounds already hold for CTL, and so we supply the upper bounds. The significance of this work is two-fold: GCTL is much more expressive than CTL as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity.

Note
Note
Stats
The PDF-Document has been downloaded 8 times.