Abstract
This paper reports on a quest for a language for expressing properties
of telecommunication services and features, which may play a part in
feature interaction detection.
A language is sought with a restricted, but practically sufficient,
expressive power, which can be complemented with computer-based tools
for verification of models described in SDL with respect to properties
expressed in the language.
A language is suggested which allows the observer technique to be used
for checking whether properties expressed in the language are satisfied
by models described in SDL.
This language can be viewed as a restricted version of the full
branching-time temporal logic ACTL*.
Electronic version.