Proving feature non-interaction with Alternating-Time Temporal Logic

Franck Cassez, Mark Ryan, Pierre-Yves Schobbens

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution


When engineers design a system with features, they wish to have methods to prove that the features do not interact in ways which are undesirable. One approach to demonstrating that features do not interact undesirably is to equip them with properties which are intended to hold of a system having the feature. In this view, a feature is a pair consisting of the implementation of the feature and a set of properties. Integrating a feature with a base system consists of modifying the base system in the way described by the feature implementation. The integration is deemed successful if the resulting system satisfies the properties of the feature (and of the base system). Evidence that a feature does not negatively interact with second feature may be obtained by verifying that introducing the second feature does not destroy the properties of the first feature.
Original languageEnglish
Title of host publicationLanguage Constructs for Describing Features
Subtitle of host publicationProceedings of the FIREworks workshop
EditorsS Gilmore, M. D Ryan
Place of PublicationLondon
Number of pages19
Publication statusPublished - 2000


  • features integration
  • features interaction
  • simulation
  • features
  • alternating-time temporal logic
  • ATL


Dive into the research topics of 'Proving feature non-interaction with Alternating-Time Temporal Logic'. Together they form a unique fingerprint.

Cite this