(April 2009)

Available formats: (none)

Filed on March 18, 2009
Updated on April 2, 2009

A framework based on the notion of \emph{conflict-tolerance} was
proposed in [DG08] as a
methodology for developing and reasoning about systems that are composed
of multiple independent features. In [DG08], the authors
use annotated transition systems to specify conflict-tolerant features.
In this paper we propose a way of specifying conflict-tolerant
features in Temporal Logic,
which is a specification language widely used in practice.
We call our logic Conflict-Tolerant LTL or CT-LTL.
We also provide an algorithm for verifying whether a given feature
implementation meets a specification given in our logic.
The paper concludes by providing a constructive procedure for
synthesising a finite-state feature implementation
from a given CT-LTL specification.

Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2009/4/.

Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]