Dining Philosopher with Host Property Specifications in CTL

This page describes the dining philosopher with host properties in Computation Tree Logic (CTL). For other property specification formalisms, click on the name of the property.

Adjacent Philosophers Not Eating property

AG ((( phil__1=s3 ) -> !( phil__2=s3 )) &

    (( phil__2=s3 ) -> !( phil__1=s3 ))) 
    

Back to Dining Philosophers with Host

Back to main