摘要: In modular verification the specification of a module consists two parts. One part describes guaranteed behavior module. The other assumed environment with which is interacting. This called assume-guarantee paradigm. Even when one specifies in branching temporal logic, assumption pair concerns interaction along each computation, and therefore often naturally expressed linear logic. this paper we consider specifications given by an LTL formula guarantee CTL formula. Verifying modules respect to such linear-branching model-checking problem. We apply automata-theoretic techniques obtain algorithm whose running time size guarantee, but doubly exponential assumption. also show that high complexity inherent proving problem EXPSPACE-complete. lower bound applies even if restricted be specified /spl forall/CTL, universal fragment CTL.
acm.org 
sci-hub.se 参考文章(37)
Cliff B. Jones, Specification and Design of (Parallel) Programs ifip congress. pp. 321- 332 ,(1983)
Bernhard Josko, Model checking of CTL formulae under liveness assumptions international colloquium on automata, languages and programming. pp. 280- 289 ,(1987) , 10.1007/3-540-18088-5_23
Bernhard Josko, Verifying the Correctness of AADL Modules Using Model Checking rex workshop on stepwise refinement of distributed systems models formalisms correctness. ,vol. 430, pp. 386- 400 ,(1989) , 10.1007/3-540-52559-9_72
Adnan Aziz, Thomas R. Shiple, Vigyan Singhal, Alberto L. Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking computer aided verification. pp. 324- 337 ,(1994) , 10.1007/3-540-58179-0_65
Bernhard Josko, MCTL - An Extension of CTL for Modular Verification of Concurrent Systems Temporal Logic in Specification. pp. 165- 187 ,(1987) , 10.1007/3-540-51803-7_25
Werner Damm, Gert Döhmen, Volker Gerstner, Bernhard Josko, Modular verification of Petri Nets Lecture Notes in Computer Science. pp. 180- 207 ,(1990) , 10.1007/3-540-52559-9_65
Dennis Dams, Orna Grumberg, Rob Gerth, Generation of Reduced Models for Checking Fragments of CTL computer aided verification. pp. 479- 490 ,(1993) , 10.1007/3-540-56922-7_39
E. Clarke, O. Grumberg, D. Long, Verification Tools for Finite-State Concurrent Systems A Decade of Concurrency, Reflections and Perspectives, REX School/Symposium. pp. 124- 175 ,(1993) , 10.1007/3-540-58043-3_19
J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in CESAR Proceedings of the 5th Colloquium on International Symposium on Programming. pp. 337- 351 ,(1982) , 10.1007/3-540-11494-7_22
E. M. Clarke, I. A. Draghicescu, Expressibility results for linear-time and branching-time logics Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop. pp. 428- 437 ,(1988) , 10.1007/BFB0013029