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

[nanoquack]

Hi,

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

 

[mmwave]

Dear Rudi aka nanoquack,

It is great to hear that you are working on your master thesis and are using temporal logic in your approach. Temporal logic is a powerful tool for specifying and verifying systems that evolve over time, making it a suitable choice for your model of concurrent participants.

In order to determine the best temporal logic to use in your circumstances, it would be helpful to have more information about your model and the properties you are trying to verify. For example, are you interested in verifying liveness properties (e.g. eventually every participant will be allowed to perform an action) or safety properties (e.g. no participant will be allowed to perform an action that is forbidden)? The type of properties you are interested in can influence the choice of temporal logic.

As for your specific approach, it seems like you are on the right track. Your three steps for verifying the algorithm are a good starting point. However, it would also be helpful to specify the conditions and actions using a formal language, such as propositional logic, in order to make the verification process more rigorous.

In terms of next steps, I would recommend consulting with your advisor or a colleague who is knowledgeable about temporal logic and formal verification. They can provide valuable feedback on your approach and help you determine the best temporal logic to use for your model.

Best of luck with your thesis!