Branching-time logics with path relativisation (Q386037)

Temporal logics are a widespread tool in specification and verification of finite state systems. Branching-time logic CTL* is one of the more expressive languages used. It extends linear temporal logic, suitable to specify temporal properties along computation paths, with path quantifiers. The present paper extends CTL* by relativized quantifiers. For this, the model of finite state systems is modified by adding labels (alphabet symbols) to edges between nodes. In this way, an infinite path in the system defines an infinite word (\(\omega\)-word), its so-called \textit{trace}. The relativized path quantifiers now quantify only over such paths whose trace is an element in a fixed \(\omega\)-language.NEWLINENEWLINEDifferent classes of \(\omega\)-languages used in quantifier relativization are considered (regular, visibly pushdown, pushdown) and for each of them, expressivity, complexity of model checking, and complexity of satisfiability are studied. For example, model checking for CTL with arbitrary pushdown language remains polynomial-time decidable, model checking for CTL* relative to regular \(\omega\)-languages remains PSPACE-complete, but becomes EXPTIME-complete for more complicated path languages.