Conflict-Tolerant Specifications in Temporal Logic
Sumesh Divakaran, Deepak D'Souza, Raj Mohan M.

IISc-CSA-TR-2009-8
(October 2009)

Available formats: pdf

Filed on October 1, 2009
Updated on October 1, 2009

Abstract
A framework based on the notion of 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/8/.

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