Satisfiability of ECTL⁎ with constraints

作者:

Highlights:

• Satisfiability for ECTL⁎ with local constraints over the integers is decidable.

• Finite satisfiability for ECTL⁎ with local constraints over the integers is decidable.

• Locality of the constraints is necessary for decidability.

摘要

•Satisfiability for ECTL⁎ with local constraints over the integers is decidable.•Finite satisfiability for ECTL⁎ with local constraints over the integers is decidable.•Locality of the constraints is necessary for decidability.

论文关键词:Temporal logics with integer constraints,ECTL*,Monadic second-order logic with the bounding quantifier

论文评审过程:Received 16 September 2014, Revised 11 December 2015, Accepted 5 February 2016, Available online 9 March 2016, Version of Record 1 April 2016.

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