by Florent Peres, Ivana Černá, August 2013, 46 pages.
FIMU-RS-2013-01. Available as Postscript, PDF.
Finding an infinite sequence of transitions (a run) going through some special states (called accepting) is of importance for fields like formal verification. Whereas finding such a sequence as been extensively studied, the problem of maintaining this sequence upon changes in the model or the specification has received less attention. In this work, we propose a solution to the maintenance of an accepting run when the transition system representing the product of the model and of the specification is changed, using the Tarjan`s algorithm as a base algorithm.