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...
| المؤلفون الرئيسيون: | , , , , |
|---|---|
| التنسيق: | Journal article |
| منشور في: |
Elsevier
2018
|
| _version_ | 1826264902842449920 |
|---|---|
| author | Fontaine, G Mogavero, F Murano, A Perelli, G Sorrentino, L |
| author_facet | Fontaine, G Mogavero, F Murano, A Perelli, G Sorrentino, L |
| author_sort | Fontaine, G |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T20:15:19Z |
| format | Journal article |
| id | oxford-uuid:2bf455a1-20f9-4c1b-bc38-dcc6f3a632a8 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T20:15:19Z |
| publishDate | 2018 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:2bf455a1-20f9-4c1b-bc38-dcc6f3a632a82022-03-26T12:34:03ZCycle detection in computation tree logicJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:2bf455a1-20f9-4c1b-bc38-dcc6f3a632a8Symplectic Elements at OxfordElsevier2018Fontaine, GMogavero, FMurano, APerelli, GSorrentino, LWe 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. |
| spellingShingle | Fontaine, G Mogavero, F Murano, A Perelli, G Sorrentino, L Cycle detection in computation tree logic |
| title | Cycle detection in computation tree logic |
| title_full | Cycle detection in computation tree logic |
| title_fullStr | Cycle detection in computation tree logic |
| title_full_unstemmed | Cycle detection in computation tree logic |
| title_short | Cycle detection in computation tree logic |
| title_sort | cycle detection in computation tree logic |
| work_keys_str_mv | AT fontaineg cycledetectionincomputationtreelogic AT mogaverof cycledetectionincomputationtreelogic AT muranoa cycledetectionincomputationtreelogic AT perellig cycledetectionincomputationtreelogic AT sorrentinol cycledetectionincomputationtreelogic |