---
res:
bibo_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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Krishnendu Chatterjee
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Pallab
foaf_name: Dasgupta, Pallab
foaf_surname: Dasgupta
- foaf_Person:
foaf_givenName: Partha
foaf_name: Chakrabarti, Partha P
foaf_surname: Chakrabarti
bibo_doi: 10.1007/978-3-540-30536-1_13
bibo_volume: 3326
dct_date: 2005^xs_gYear
dct_publisher: Springer@
dct_title: Complexity of compositional model checking of computation tree logic
on simple structures@
...