Modeling Product Lines with Kripke Structures and Modal Logic

Abstract—Product lines (PLs) are now an established frame-work for software design. For formal analysis of PLs, they are usually specified by propositional theories (PT) with Boolean se-mantics. We discuss a major deficiency of the PL2PT-translation, and show that it can be fixed by considering a product as an instantiation process rather than its final result. Correspondingly, models of PLs can be viewed as special Kripke structures specifiable by a suitable version of modal logic. We also discuss intriguing similarities between PL modeling and event-based models for concurrency. I