Author(s):

Henzinger, Thomas A; Kupferman, Orna; Rajamani, Sriram K

Title: 
Fair simulation

Title Series: 
LNCS

Affiliation 

Abstract: 
The simulation preorder for labeled transition systems is defined locally as a game that relates states with their immediate successor states. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We extend the local definition of simulation to account for fairness: system S fairly simulates system I iff in the simulation game, there is a strategy that matches with each fair computation of I a fair computation of S. Our definition enjoys a fully abstract semantics and has a logical characterization: S fairly simulates I iff every fair computation tree embedded in the unrolling of I can be embedded also in the unrolling of S or, equivalently, iff every FairAFMC formula satisfied by I is satisfied also by S (AFMC is the universal fragment of the alternationfree calculus). The locality of the definition leads us to a polynomialtime algorithm for checking fair simulation for finitestate systems with weak and strong fairness constraints. Finally, fair simulation implies fair tracecontainment, and is therefore useful as an efficientlycomputable local criterion for proving lineartime abstraction hierarchies.

Conference Title:

CONCUR: Concurrency Theory

Volume: 
1243

Conference Dates:

July 1–4, 1997

Conference Location:

Warsaw, Poland

ISBN:

9783959770170

Publisher:

Schloss Dagstuhl  LeibnizZentrum für Informatik

Date Published:

19970101

Start Page: 
273

End Page:

287

DOI: 
10.1007/3540631410_19

Notes: 
This research was supported in part by the ONR YIP award N000149510520, by the NSF CAREER award CCR9501708, by the NSF grant CCR9504469, by the AFOSR contract F496209310056, by the ARO MURI grant DAAH049610341, by the ARPA grant NAG2892, and by the SRC contract 95DC324.036.

Open access: 
no 