Which branching-time properties are effectively linear?
Three types of linearity notions for formulas of branching-time temporal logic CTL* are presented: equi-linearity, sub-linearity and strong linearity. Each type of linearity is defined in terms of relationships between models that satisfy a formula of that type. These three types coincide for linear-time temporal logic LTL, whereas considering them under a branching-time context the three notions turn out to be distinct and can be ordered by inclusion. Each class of formulas is examined with respect to models that include fairness constraints. It is shown that membership in a linearity class is preserved under removal of fairness; however, going the other way round, that is, adding fairness, can strictly reduce membership in a linearity class. For the particular subset \(\forall\)CTL* of CTL*, it is proven that the classes of equi-linear and sub-linear formulas coincide, and a syntactic characterization of formulas in the class is provided.
- scientific article; zbMATH DE number 1536555
- From linear time to branching time
- Branching vs. Linear Time: Semantical Perspective
- Axioms for Branching Time
- scientific article; zbMATH DE number 1304989
- Linear-Time Model Checking Branching Processes
- From branching to linear time, coalgebraically
- From branching to linear time, coalgebraically
- The quantitative linear-time-branching-time spectrum
This page was built for publication: Which branching-time properties are effectively linear?
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2720312)
