Complexity of compositional model checking of computation tree logic on simple structures Conference Paper

Author(s): Chatterjee, Krishnendu; Dasgupta, Pallab; Chakrabarti, Partha P
Title: Complexity of compositional model checking of computation tree logic on simple structures
Title Series: LNCS
Abstract: Temporal Logic Model Checking is one of the most potent tools for the verification of finite state systems. Computation Tree Logic (CTL) has gained popularity because unlike most other logics, CTL model checking of a single transition system can be achieved in polynomial time. However, in most real-life problems, specially in distributed and parallel systems, the system consist of a set of concurrent processes and the verification problem translates to model check the composition of the component processes. Since explicit composition leads to state explosion, verifying the system without actually composing the components is attractive, even for possibly restrictive class of systems. We show that the problem of compositional CTL model checking is PSPACE complete for the class of systems composed of components that are tree-like transition structure and do not interact among themselves. For the simplest forms of existential and universal CTL formulas model checking turns out to be NP complete and coNP complete, respectively. The results hold for both synchronous and asynchronous composition.
Conference Title: IWDC: International Workshop on Distributed Computing
Volume: 3326
Conference Dates: December 27-30, 2004
Conference Location: Kolkata, India
ISBN: 978-3-540-24076-1
Publisher: Springer  
Date Published: 2005-02-14
Start Page: 89
End Page: 102
Sponsor: Pallab Dasgupta and P.P.Chakrabarti thank the Dept. of Science & Tech., Govt. of India, for partial support of this work
DOI: 10.1007/978-3-540-30536-1_13
Open access: no
IST Austria Authors
Related IST Austria Work