Abstract | ||
---|---|---|
This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along
paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct
logics generalizing CTL. We provide a thorough analysis of their expressiveness and of the complexity of their model-checking problem (ranging from
P-complete to undecidable).
|
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-12032-9_15 | Logical Methods in Computer Science |
Keywords | DocType | Volume |
temporal logic,quantitative extension,model-checking problem,arithmetic operation,temporal modality,distinct logic,thorough analysis,certain sub-formulas | Journal | 9 |
Issue | ISSN | ISBN |
1 | Logical Methods in Computer Science, Volume 9, Issue 1 (February
15, 2013) lmcs:1058 | 3-642-12031-8 |
Citations | PageRank | References |
3 | 0.38 | 20 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
François Laroussinie | 1 | 7 | 0.77 |
Antoine Meyer | 2 | 79 | 4.69 |
Eudes Petonnet | 3 | 3 | 0.38 |