Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
11021130 | Information and Computation | 2018 | 15 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Gaëlle Fontaine, Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Loredana Sorrentino,