Files

Abstract

We present a method that allows to guarantee liveness by construction of a class of timed systems. The method is based on the use of a set of structural properties which can be checked locallyat low cost. We provide sufficient conditions for liveness preservation byparallel composition and prioritychoice operators. The latter allow to restrict a system's behavior according to a given priorityorder on its actions. We present several examples illustrating the use of the results, in particular for the construction of live controllers

Details

Actions

Preview