LTL, CTL or TLA for modelling for my model (detailed description inside)?

Question

I am currently writing my master thesis and am confronted with specifying and verifying my approach in a temporal logic.

Which temporal logic would be the best to use in my circumstances? I would really like some feedback on my approach and how to proceed

My model consists of participants, which will be executed concurrently. For each participant, one can register rules. They look something like this:

conditions -> action

e.g.

received(a, c) ^ received(b,c) -> allowed(c,d) 

which means that c has to have received a message from b and one from c in order to be allowed to send a message to d.

Before one of the participants sends or receives a message, my prototype checks if the participant is allowed to perform that action. So far, I want to verify that the algorithm does the following:

1. If no rule exists whose conditions hold: forbid the action

2. If a rule exists whose the conditions hold and it forbids the action: forbid the action

3. If a rule exists whose conditions hold, it allows the action and no other rule exists whose condition holds and that forbids the action: allow the action

Answer 1

It looks like that you want to find out if some properties of your specification are invariants. That is, if during the execution of the program the properties are always true.

The concept of invariant can be expressed in all the temporal logic formalisms. However, I would use TLA+ because there is a model checker, a proof system available, an active community, and a couple of excellent books for writing specifications.

But... be aware, Temporal Logic is not a piece of cake, and you will need to spend some quality time reading and thinking carefully.

Answer 2

There is a misconception in comparing these three logics. The temporal logic in both TLA+ and LTL is linear. TLA+ includes set theory, and the axioms of TLA+ are based on Zermelo-Fraenkel set theory. TLA+ syntactically enforces stutter-invariance (for ensuring that refinement is practical). LTL is a propositional logic.

CTL is drastically different from LTL, because CTL is a branching time logic, whereas LTL a linear time logic. A single sequence is a model for a linear-time formula. In contrast, a tree is a model for a branching-time formula. A sequence represents a single execution, whereas a tree represents many executions, that start at some state.

Path quantification is available in CTL, whereas absent from LTL. There's a common subset of LTL and CTL, but they are incomparable (= some properties are expressible in LTL only, others in CTL only). CTL* is their common superset.

For the application that you sketch, linear-time semantics appears more suitable. I would recommend using TLA+, because it offers a good discipline for describing systems, and is temporally sufficiently expressive that you probably won't need LTL (the other way around: if you can't specify the system with a stutter-invariant formula in TLA+, then it's more likely that the system needs revision, rather than the full expressive power of LTL being necessary).

The TLA+ book is a very readable introduction.