Specification and verification of modal properties for structured systems