Reader/Writer Property Specifications in CTL

This page describes the reader/writer properties in Computation Tree Logic (CTL). For other property specification formalisms, click on the name of the property.

Exclusive-write property

AG ((( writer_1 = s2 ) -> !( writer_2 = s2 )) &
    (( writer_2 = s2 ) -> !( writer_1 = s2 )))
    

Write-first property

AG ( reader_1_read -> any_writer_wrote ) 
    

Back to Readers/Writers

Back to main