Proof planning for feature interactions: A preliminary report

Claudio Castellini, Alan Smaill

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


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.
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
Number of pages13
ISBN (Electronic)978-3-540-36078-0
ISBN (Print)978-3-540-00010-5
Publication statusPublished - 2002

Publication series

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

Fingerprint Dive into the research topics of 'Proof planning for feature interactions: A preliminary report'. Together they form a unique fingerprint.

Cite this