Model checking of pushdown systems for projection temporal logic

作者：Zhao, Liang; Wang, Xiaobing; Duan, Zhenhua^*

来源：Theoretical Computer Science, 2019, 774: 82-94.

DOI：10.1016/j.tcs.2016.06.031

• Model checking
• Algorithm and complexity
• Pushdown system
• Projection temporal logic
• Full regular expressiveness

In this paper, we study the model checking problem of pushdown systems for projection temporal logic (PTL), an interval-based temporal logic that is as expressive as the full regular languages. For this, we provide an algorithm to decide whether a pushdown system, determined by a pushdown automaton, satisfies a desired logic property, by using relevant automata notations and operations. The algorithm terminates in exponential time for normal PTL properties, i.e. properties specified as normal PTL formulas. To show the lower bound of complexity of the model checking problem, we also construct a polynomial-time reduction from the acceptance problem of a linearly bounded alternating Turing machine. As a result, the model checking problem of pushdown systems for normal PTL properties is EXPTIME-complete.

• 出版日期2019-6-25
• 单位西安电子科技大学