Show simple item record

dc.contributor.authorKupferman, Orna
Vardi, Moshe Y.
Wolper, Pierre
dc.date.accessioned 2017-08-02T22:03:39Z
dc.date.available 2017-08-02T22:03:39Z
dc.date.issued 1998-02-22
dc.identifier.urihttps://hdl.handle.net/1911/96485
dc.description.abstract 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 CTLand is 2EXPTIME-complete for specifications in ctls. 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.
dc.format.extent 24 pp
dc.language.iso eng
dc.rights You are granted permission for the noncommercial reproduction, distribution, display, and performance of this technical report in any format, but this permission is only for a period of forty-five (45) days from the most recent time that you verified that this technical report is still available from the Computer Science Department of Rice University under terms that include this permission. All other rights are reserved by the author(s).
dc.title Module Checking
dc.type Technical report
dc.date.note February 22, 1998
dc.identifier.digital TR98-302
dc.type.dcmi Text
dc.identifier.citation Kupferman, Orna, Vardi, Moshe Y. and Wolper, Pierre. "Module Checking." (1998) https://hdl.handle.net/1911/96485.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record