Welcome to our community

Be a part of something great, join today!

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


New member
Mar 3, 2014

I am currently writing my master thesis and am confronted with specifying and verifying my approach in a temporal logic. I will shortly explain the basic scenario, but feel free to ask for details ;-) Basically I'm wondering which temporal logic would be the best to use in my circumstances and also 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 that:
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

Kind Regards to all of You,
Rudi aka nanoquack