Edinburgh Research Explorer

Proof planning for feature interactions: A preliminary report

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
Subtitle of host publication9th International Conference, LPAR 2002 Tbilisi, Georgia, October 14–18, 2002 Proceedings
PublisherSpringer Berlin Heidelberg
Pages102-114
Number of pages13
ISBN (Electronic)978-3-540-36078-0
ISBN (Print)978-3-540-00010-5
DOIs
Publication statusPublished - 2002

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume2514
ISSN (Print)0302-9743

Abstract

We report on an initial success obtained in investigating the Feature Interaction problem (FI) via proof planning. FIs arise as an unwanted/unexpected behaviour in large telephone networks and have recently attracted interest not only from the Computer Science community but also from the industrial world. So far, FIs have been solved mainly via approximation plus finite-state methods (model checking being the most popular); in our work we attack the problem via proof planning in First-Order Linear Temporal Logic (FOLTL), therefore making use of no finite-state approximation or restricting assumption about quantification. We have integrated the proof planner λCLAM with an object-level FOLTL theorem prover called FTL, and have so far re-discovered a feature interaction in a basic (but far from trivial) example.

ID: 23594040