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:
If no rule exists whose conditions hold: forbid the action
If a rule exists whose the conditions hold and it forbids the action: forbid the action
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
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.