L: Talk to Daniel Bond L: Need to produce printed version by June 9 - Talk to uniprint and ask how much time they need [2 weeks to be safe] L: Want PDFs without pagenumbers J: Schedule for 2008 ... M: Add column (2) Thesis tasks, as well as (3) Delivery Events T: Can also consider FSTTCS J: Modal mu calculus references? T: Green Book, Language ... Automata ... 2003 Mads Dam for CTL* embedding in to mu-C J: fixed point extentions to CTL*? M: state fixed points = QCTL* = non-elementary M: Also path fixed points /LTL M: Funding for trip harder than originally expected M: want expected funds required soon Itenery and Budget M: ARC grant will run out at some point. M: How long does hackett scholarship last? M: Can use remaining $1000 for trip? M: seminars diff time Meet same time next week (Fri Noon) -- Introduction RoCTL*, a branching time logic of robustness We present the syntax and semantics of a new temporal logic of robustness, RoCTL*, and show that this logic is decidable Additionally we present bundled tree semantics for this systax, producing a logic we call RoBCTL* Deontic issues Applications of RoCTL* Network protocols. Resource systems A Tableaux for RoBCTL* We present a tableaux for RoBCTL*, and show that this Tableaux performs well for a interesting syntatic restriction of ROBCTL* Restricted logics In the last chapter we introduced a restriction ??? of RoBCTL*. In this chapter we discuss more restrictions of RoBCTL* and RoCTL* logics, and discuss where such logics are useful. One such logic is RoCTL, a CTL like restriction of RoCTL*. Another such restriction is: An embedding of RoCTL* in modal mu calculus. We present a embedding of RoCTL* into the modal mu calculus. This embedding provides further information on the expressivity and complexity of RoCTL*. Axiomitisation of RoBCTL*/RoCTL* Axiom systems allow simple proofs of the validity of formulae. Another chapter Possibly insert a discussion of expressivity, a philosophical discussion of RoCTL* interpretation of Deontic operators model-checking or other result. Benchmarks We have presented a number of decision procedures for RoCTL* and similar logics. Often the theoretical worst case performance of a decision procedure is less important than the time taken to decide typical formulae. Here we present discussion of benchmarks of sample implementions of the Decision procedures discussed in this thesis. Conclusions an alter nd 2.1 Syntax Decidability