Show simple item record

dc.contributor.authorKupferman, Orna
Vardi, Moshe Y.
dc.date.accessioned 2017-08-02T22:03:33Z
dc.date.available 2017-08-02T22:03:33Z
dc.date.issued 1997-08-27
dc.identifier.urihttps://hdl.handle.net/1911/96470
dc.description.abstract In program verification we check that an implementation meets its specification. Both the specification and the implementation describe the possible behaviors of the program, though at different levels of abstraction. We distinguish between two approaches to implementation of specifications. The first approach is trace-based implementation, where we require every computation of the implementation to correlate to some computation of the specification. The second approach is tree-based implementation, where we require every computation tree embodied in the implementation to correlate to some computation tree embodied in the specification. The two approaches to implementation are strongly related to the linear-time versus branching-time dichotomy in temporal logic. In this work we examine the trace-based and the tree-based approaches from a complexity-theoretic point of view. We consider and compare the complexity of verification of fair transition systems, modeling both the implementation and the specification, in the two approaches. We consider unconditional, weak, and strong fairness. For the trace-based approach, the corresponding problem is fair containment. For the tree-based approach, the corresponding problem is fair simulation. We show that while both problems are PSPACE-complete, their complexities in terms of the size of the implementation do not coincide and the trace-based approach is easier. As the implementation is normally much bigger than the specification, we see this as an advantage of the trace-based approach. Our results are at variance with the known results for the case of transition systems with no fairness, where no approach is evidently advantageous.
dc.format.extent 37 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 Verification of Fair Transition Systems
dc.type Technical report
dc.date.note August 27, 1997
dc.identifier.digital TR97-286
dc.type.dcmi Text
dc.identifier.citation Kupferman, Orna and Vardi, Moshe Y.. "Verification of Fair Transition Systems." (1997) https://hdl.handle.net/1911/96470.


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record