Quantified Computation Tree Logic |
| |
Authors: | AC PatthakI Bhattacharya A Dasgupta Pallab DasguptaPP Chakrabarti |
| |
Affiliation: | Department of Computer Science and Engineering, Indian Institute of Technology, Kharagpur, India 721302 |
| |
Abstract: | Computation Tree Logic (CTL) is one of the most syntactically elegant and computationally attractive temporal logics for branching time model checking. In this paper, we observe that while CTL can be verified in time polynomial in the size of the state space times the length of the formula, there is a large set of reachability properties which cannot be expressed in CTL, but can still be verified in polynomial time. We present a powerful extension of CTL with first-order quantification over sets of reachable states. The extended logic, QCTL, preserves the syntactic elegance of CTL while enhancing its expressive power significantly. We show that QCTL model checking is PSPACE-complete in general, but has a rich fragment (containing CTL) which can be checked in polynomial time. We show that this fragment is significantly more expressive than CTL while preserving the syntactic beauty of CTL. |
| |
Keywords: | Computation Tree Logic Model checking Verification |
本文献已被 ScienceDirect 等数据库收录! |
|