The various temporal logics are particularly suitable for the specification and verification of concurrent computer programs. Are there logics that are particularly suitable for the specification and verification of multi-agent and distributed systems and algorithms? Or are the temporal logics used as-is for these purposes as well?
1 Answer
TLA+ is commonly used for verification of distributed algorithms. I've seen it actively used by researchers and industry engineers/architects.