[HN Gopher] An introduction to temporal logic and how it can be ...
___________________________________________________________________
An introduction to temporal logic and how it can be used to analyze
concurrency
Author : eigenvalue
Score : 80 points
Date : 2024-01-22 20:21 UTC (2 days ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| eigenvalue wrote:
| I recently started learning about this subject, which is pretty
| interesting. I had heard about it a while ago, but didn't know
| much about it besides the basics, and certainly didn't know how
| it could be applied to real problems since it always seemed
| pretty abstract. While I did learn about classical logic in
| college many years ago, I also recently gave myself a refresher
| on FOL and its axioms and inference rules so I could better
| understand how temporal logic departs from FOL and builds on it.
|
| Anyway, in an attempt to help me learn the material better, I
| decided to write up the basic ideas along with several examples
| of how it could be applied. Perhaps it will be of interest to you
| as well, although there is certainly nothing new or
| groundbreaking in my exposition. I did try very hard to make
| things as simple and concrete as I could while not getting too
| "hand wavy" as they say.
|
| Caveat: I'm certainly no expert in this field, so if you spot any
| mistakes, please let me know and I'll revise it (or just submit a
| PR on GitHub!).
| azaras wrote:
| I am also starting to learn, and I don't know if it can be
| applied to my real problems.
|
| I chose the Lamport learning path. I love that guy and how he
| thinks and writes. I am reading the book (I bought it in paper,
| but there is a free version online), watching the video
| courses, and reading the PlusCal tutorial online.
|
| I enjoy the path and the enlightenment when describing a system
| with math. Human language has too many ambiguities, very little
| precision, and is verbose to express some ideas.
| klabb3 wrote:
| Which book? I haven't read anything of him. But whenever I
| see his stuff, I've been happy to see that it's not just
| academic, but understandable and useful for solving real
| problems.
| scriptnull wrote:
| The book is probably "Specifying Systems" by Leslie
| Lamport[1].
|
| I recently started reading this book and felt amazed at the
| way it progresses. It introduces Propositional logic,
| Predicate logic, and then Temporal logic. Enjoyed it so far
| and looking to apply it in the real-world.
|
| [1] https://lamport.azurewebsites.net/tla/book.html
| azaras wrote:
| You are right, that one.
| zozbot234 wrote:
| Strictly speaking, temporal logic does not so much 'depart'
| from FOL. It's a modality, hence like other modal logics it can
| be viewed as a restriction of full FOL (where the domain of
| discourse can be seen as some notion of 'possible worlds') with
| some desirable properties such as better computational
| tractability.
| Garlef wrote:
| Are there similar systems where the notion of time is not global?
| actionfromafar wrote:
| That could have very interesting implications for high
| performance computing. Think clock drift, fast interchip
| communications and clusters.
| pavlov wrote:
| For a more automated way to model and verify concurrency using
| temporal logic as one tool, see TLA+:
|
| https://en.wikipedia.org/wiki/TLA%2B
| sylware wrote:
| That let me think about all the programmers who think,
| intuitively, that circular buffers with atomic read and write
| pointers have an easy 'concurrency-safe' proof...
| actionfromafar wrote:
| It feels great knowing someone is thinking of me.
| sylware wrote:
| trap
| yodsanklai wrote:
| Concurrent algorithms are notoriously hard. There's been tons of
| academic work to build models/language for concurrency, tools to
| check properties and so on.
|
| Yet, it seems nothing has emerged that practitioners actually
| use. I know that there are some occasional experiments (such
| industrial team specified their protocols using TLA+/Alloy), but
| it's still extremely limited. I wonder why that is.
| eigenvalue wrote:
| We need automated ways of converting Python and other popular
| languages to TLA+ with ways of verifying that they were
| translated correctly. Otherwise it seems like too much work for
| most purposes.
| zozbot234 wrote:
| TLA+ is not intended for end-to-end verification of actually
| running code, that's still the domain of type systems and
| interactive proof checkers. You're "specifying" a toy model
| of how your system will behave and then verifying that.
| eigenvalue wrote:
| Right. But even the automatic translation/conversion from
| the "real" Python code (or whatever it is) to the toy model
| of that code would make TLA+ a lot more accessible and
| useful to millions of developers instead of the couple
| hundred at most (just a guess, maybe it's more?) that
| currently make serious use of it.
|
| I understand that TLA+ is not really intended for that and
| it's currently used more for super important, mission
| critical applications like flight computer code, but I
| would love to see that level of care and attention brought
| to more typical software, which even in relatively "boring"
| applications can involve a lot of concurrency nowadays.
| zozbot234 wrote:
| A toy model of existing Python code is... a type system,
| which Python has. TLA+ is appropriate for cases where you
| don't even have that.
| taeric wrote:
| Modeling an entire system is almost always harder than modeling
| individual pieces of a system. As such, I expect that you
| almost always start with individual parts modeled, and then you
| are trying to combine multiple models together.
|
| Stated differently, no model can really account for
| interactions that are invisible to it. As such, unless you are
| aiming at a giant model that encompasses everything, it seems
| unlikely that you will be able to use some modeling tools that
| are made to do this sort of stuff directly.
| Taikonerd wrote:
| I think most development occurs on problems that can't be
| formally modeled anyway. Most developers work on things like,
| "can you add this feature to the e-commerce site? And can the
| pop-up be blue?" which isn't really model-able.
|
| But that's not to say that formal methods are useless! We can
| still prove some interesting aspects of programs -- for
| example, that every lock that gets acquired later gets
| released. I think tools like Infer[0] could become common in
| the coming years.
|
| [0]: https://fbinfer.com/
| Horffupolde wrote:
| >English: "It is necessary and sufficient for the ground to be
| wet that it is raining."
|
| That's not true.
| eigenvalue wrote:
| When you're using FOL, there is an understanding that it's not
| trying to literally describe the world accurately-- it's an
| idealized version to demonstrate logical thinking in a way
| that's easier and more intuitive than only using symbols like P
| or Q. So when there is a syllogism involving "All birds can
| fly," no one is seriously claiming that there aren't any birds
| that have damaged wings or that are too weak to fly.
| hwayne wrote:
| > First, let's prove that a certain protocol ensures that no
| philosopher will starve. Starvation occurs when a philosopher is
| perpetually denied access to resources (in this case, forks), and
| thus can never eat. We'll use a protocol where a philosopher must
| pick up both forks at once or put down any fork they've picked up
| and wait before trying again.
|
| This doesn't actually guarantee starvation freedom. Consider a
| scenario with three philosophers: Plato, Hume, and Arendt. Plato
| needs forks HA, Hume needs forks PA, etc.
|
| 1. Plato picks up forks HA and starts eating.
|
| 2. Hume picks up P, fails to pick up A. Hume immediately puts
| down P and enters the waiting phase.
|
| 3. Plato puts down HA.
|
| 4. Arendt picks up HP and starts eating.
|
| 5. Hume exits waiting phase.
|
| 6. Hume picks up A, fails to pick up P. Hume immediately puts
| down H and enters the waiting phase.
|
| 7. GOTO 1
|
| The problem is that there's no guarantee of "strong fairness":
| that if the system _keeps returning_ to a state where Hume can
| pick up both forks, he is guaranteed to eventually pick up both
| forks.
|
| Unrelated, but this is formalism is more precisely known as "
| _linear_ temporal logic ". That's because there are many
| different temporal logics! Temporal logics are "modal" logics,
| which means it's a logic equipped with the "necessarily" and
| "possibly" modifiers. The "necessarily" easily maps onto temporal
| logic: it just means "true at all times". But what does
| "possibly" mean?
|
| If I flip a coin, is it "possibly heads?"
|
| In linear temporal logic, the answer is "no", because there are
| sequences of events where the coin is never heads. In computation
| tree logic, the answer is "yes", because the timeline has a
| branch where it lands heads.
|
| Lamport wrote an article arguing that LTL is more useful in the
| context of programming
| (https://dl.acm.org/doi/pdf/10.1145/567446.567463). He'd later go
| on to make TLA, which is a restricted variant of LTL.
| eigenvalue wrote:
| Wow, thanks for catching that! I've attempted to fix the proof
| based on your comment:
|
| https://github.com/Dicklesworthstone/introduction_to_tempora...
___________________________________________________________________
(page generated 2024-01-24 23:02 UTC)