Branching-time logics with path relativisation

作者：

Highlights：

• We relativise path quantifier in branching-time logics using ω-languages.

• The extended logics are based on CTL, CTL+, CTL⁎, and ΔPDL.

• We study expressivity and complexity of satisfiability and model checking.

• Path relativisation captures abstractions and refinements of large systems.

• Logics with non-regular relativisations may be useful for software synthesis.

摘要

•We relativise path quantifier in branching-time logics using ω-languages.•The extended logics are based on CTL, CTL+, CTL⁎, and ΔPDL.•We study expressivity and complexity of satisfiability and model checking.•Path relativisation captures abstractions and refinements of large systems.•Logics with non-regular relativisations may be useful for software synthesis.

论文关键词：Temporal logic,CTL⁎,Formal languages,Expressive power,Model checking,Satisfiability

论文评审过程：Received 2 November 2010, Revised 2 February 2012, Accepted 4 April 2013, Available online 17 May 2013.

论文官网地址：https://doi.org/10.1016/j.jcss.2013.05.005