Cycle detection in computation tree logic
We introduce Cycle-CTL, an extension of CTL with cycle quantifications that are able to predicate over cycles. The introduced logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL and is orthogonal to μCalculus. We also give an evidence of its usefulness by providing f...
| Main Authors: | , , , , |
|---|---|
| Format: | Journal article |
| Published: |
Elsevier
2018
|
| Summary: | We introduce Cycle-CTL, an extension of CTL with cycle quantifications that are able to predicate over cycles. The introduced logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL and is orthogonal to μCalculus. We also give an evidence of its usefulness by providing few examples involving non-regular properties. We extensively investigate both the model-checking and satisfiability problems for Cycle-CTL and some of its variants/fragments. |
|---|