Dining Philosopher with Dictionary Property Specifications in CTL

This page describes the dining philosopher with dictionary 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 ))) 
    

Not Eating While Holding Dictionary property

SPEC
  AG (( phil_2=s3 ) -> !holding_dictionary )

or 

FAIRNESS
  ( phil__2=s1)
SPEC
  AG (( phil__2=s6 ) -> A [ !( phil__2=s4 ) U ( phil__2=s1 ) ] )
    

Back to Dining Philosophers with Dictionary

Back to main