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