Cutoff Results for Guarded Protocols
Date:
Tuesday, March 21, 2017 17:00 - 18:30
Speaker:
Swen Jacobs (Saarland University)
Location:
Seminar room Ground floor / Office Bldg West (I21.EG.128)
Series:
RiSE Seminar
Host:
Tom Henzinger
Contact:
NOVOTNY Petr
Guarded protocols, as introduced by Emerson and Kahlon (2000), describe concurrent systems where transitions of processes are enabled or disabled depending on the existence of other processes in certain local states. Cutoff results reduce reasoning about systems with an arbitrary number of processes to systems of a determined, fixed size. Our work is based on the observation that the existing cutoff results are i) of limited use for liveness properties because the reductions do not preserve fairness, and ii) in many cases give a prohibitively large cutoff. We provide new cutoff results that work under fairness assumptions, and prove tightness or asymptotic tightness for cutoffs that only depend on the size of the process templates. I will also report on ongoing work to obtain smaller cutoffs by considering additional static properties of the process templates, such as the number of different guards that are used in the template.