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

Chatterjee, Krishnendu ; Dasgupta, Pallab ; Chakrabarti, P. P. (2005) Complexity of compositional model checking of computation tree logic on simple structures Lecture Notes in Computer Science, 3326 . pp. 89-102. ISSN 0302-9743

[img]
Preview
PDF - Author Version
196kB

Official URL: http://www.springerlink.com/content/5jb7b9067p3lph...

Related URL: http://dx.doi.org/10.1007/978-3-540-30536-1_13

Abstract

Temporal Logic Model Checking is one of the most potent tools for the veri.cation of .nite 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 veri.cation 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.

Item Type:Article
Source:Copyright of this article belongs to Springer-Verlag.
ID Code:6015
Deposited On:19 Oct 2010 09:50
Last Modified:16 May 2016 16:26

Repository Staff Only: item control page