Proving feature non-interaction with Alternating-Time Temporal Logic

[CassezRyanSchobbens2001] Franck Cassez, Mark Ryan and Pierre-Yves Schobbens. Proving feature non-interaction with Alternating-Time Temporal Logic. In Stephen Gilmore and Mark Ryan (editors) Language Constructs for Describing Features, Springer. 2001.
Links: [Google] [Google Scholar] [CiteSeer]
Available from: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/00-atl.ps.gz