Please use this identifier to cite or link to this item:
Title: Bridging the gap between fair simulation and trace inclusion
Authors: Kesten, Yonit
Piterman, Nir
Pnueli, Amir
First Published: 25-Apr-2005
Publisher: Elsevier
Citation: Information and Computation, 2005, 200 (1), pp. 35-61.
Abstract: The paper considers the problem of checking abstraction between two finite-state fair discrete systems. In automata-theoretic terms this is trace inclusion between two nondeterministic Streett automata. We propose to reduce this problem to an algorithm for checking fair simulation between two generalized Büchi automata. For solving this question we present a new triply nested μ-calculus formula which can be implemented by symbolic methods. We then show that every trace inclusion of this type can be solved by fair simulation, provided we augment the concrete system (the contained automaton) by an appropriate ‘non-constraining’ automaton. This establishes that fair simulation offers a complete method for checking trace inclusion for finite-state systems. We illustrate the feasibility of the approach by algorithmically checking abstraction between finite state systems whose abstraction could only be verified by deductive methods up to now.
DOI Link: 10.1016/j.ic.2005.01.006
ISSN: 0890-5401
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: Copyright © 2005 Elsevier Inc. Deposited with reference to the publisher's archiving policy available on the SHERPA/RoMEO website. NOTICE: this is the author’s version of a work that was accepted for publication in Information and Computation. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Information and Computation, 2005, 200 (1), pp. 35-61. DOI# 10.1016/j.ic.2005.01.006
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
all.pdf455.79 kBUnknownView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.