Article (Scientific journals)
Module checking
Kupferman, Orna; Vardi, Moshe Y; Wolper, Pierre
2001In Information and Computation, 164 (2), p. 322-344
Peer Reviewed verified by ORBi
 

Files


Full Text
KVW01-IC.pdf
Author postprint (306.94 kB)
Download
Full Text Parts
KVW01-IC.pdf
Publisher postprint (232.04 kB)
Request a copy

All documents in ORBi are protected by a user license.

Send to



Details



Abstract :
[en] In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2EXPTIME-complete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems. (C) 2001 Academic Press.
Disciplines :
Computer science
Mathematics
Author, co-author :
Kupferman, Orna;  Hebrew University of Jerusalem > School of Computer Science and Engineering
Vardi, Moshe Y;  Rice University > Dept. of Computer Science
Wolper, Pierre  ;  Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
Language :
English
Title :
Module checking
Publication date :
2001
Journal title :
Information and Computation
ISSN :
0890-5401
eISSN :
1090-2651
Publisher :
Academic Press, San Diego, United States - California
Volume :
164
Issue :
2
Pages :
322-344
Peer reviewed :
Peer Reviewed verified by ORBi
Available on ORBi :
since 14 August 2009

Statistics


Number of views
92 (10 by ULiège)
Number of downloads
407 (3 by ULiège)

Scopus citations®
 
130
Scopus citations®
without self-citations
118
OpenCitations
 
93

Bibliography


Similar publications



Contact ORBi