About Me

Wednesday, October 1, 2008

CompSys705 tutorial

Tutorial for test tomorrow night. CCS is separate from CTL and Kripke Structure. CCS is a way to describe the actions of processes. CTL takes a Kripke Structure and unfolds it in time (modal). Labelling of a transition system is "labelling" a state with a proposition that is true. When checking a Kripke Structure, label all the states on a diagram.

NCES. Firing groups. Better to know how to use ViVe. Forced or independent transitions. Forced transitions are made by transition boxes with an event arc to it. Independent transitions can fire whenever the number of tokens in a place is satisfied or based on a rule for a transition box.