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?
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
TLA+ is commonly used for verification of distributed algorithms. I've seen it actively used by researchers and industry engineers/architects.
