1
vote
Logics for multi-agent and distributed systems and algorithms
TLA+ is commonly used for verification of distributed algorithms. I've seen it actively used by researchers and industry engineers/architects.
1
vote
What is the Kripke semantic for a linear temporal logic?
tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind.
Details:
Let $P$ be a set of atomic proposition. Write $\Sigma$ for $P$'s powerset. Write $T$ for ...
- 663
1
vote
Accepted
Which temporal logic is the one described in Manna & Pnueli's "The Temporal Logic of Reactive and Concurrent Systems: Specification"?
LTL.
PS The very book you mention has a historical note section discussing various other temporal logics near page 271.
Edit (leaving the above intact for the comments to make sense): None of the ...
- 663
Only top scored, non community-wiki answers of a minimum length are eligible