about time for some temporal logic [haha LMAO...]
Well, I'm embarassed to post this, but in response to a friend's problems with finding happiness in life; I posted the following comment to his blog:
I understand the need to exhaust all your options before making a state transition, therefore I've come up with some CTL statements to live by:
If the glass is empty: A[alive U dead]
If the glass is half full: A[(alive -> (AG EF happy)) U dead]
If the glass is always full: dead -> (AG happy)
PS: Greenberg/Leo -- I know what you're saying; they may not be tautologies but they certainly cannot be disproved for certain acceptable bounds! (e.g. if you are old enough to get alzheimers, as long as your last memory was a good one, they hold)
Oh man, I need to get out of academia... and I need to get some sleep.
I understand the need to exhaust all your options before making a state transition, therefore I've come up with some CTL statements to live by:
If the glass is empty: A[alive U dead]
If the glass is half full: A[(alive -> (AG EF happy)) U dead]
If the glass is always full: dead -> (AG happy)
PS: Greenberg/Leo -- I know what you're saying; they may not be tautologies but they certainly cannot be disproved for certain acceptable bounds! (e.g. if you are old enough to get alzheimers, as long as your last memory was a good one, they hold)
Oh man, I need to get out of academia... and I need to get some sleep.
4 Comments:
I'm not sure how I feel about dead -> (AG happy), since dead states are terminating states. Most people don't worry about termination in MC (since they're using reactive systems/concurrent protocols anyway), but this is a pretty clear case of it. I mean, the movie is called 'The Terminator'. It's not called the 'The SCC Connector'.
I can envision a contrived model where there's some state loop after a dead state, but I don't think you'd ever get me to agree that it appropriately models.
As for bounds, I don't think that's the issue. I mean, the first should be pretty easy to prove for a model simply because states are either alive or dead, so we don't need MC for that. As for the second, you just give a model and check it.
Lastly, I would write the middle property as A[(EF happy) U dead] The alive is redundant, and the AG is a little hopeful. Some people are never satisfied.
I take it back, the AG isn't just hopeful, it's unnecessary. You're already inside an AU, so if you're not dead you keep searching.
Moreover, any SCC in a model of life would imply that there was some way to live forever. This is why MC is very limited. Apparently some work is being done on push-down verification, but I haven't read anything.
P.S. Dork dork dork, dork dork, dork dorkdork. Dorkity dork, dork dork.
I totally read RBG's blog + comment two seconds before reading this entry. Trippy. And I have to second Michael Greenberg.
Dork dork dork, dork dork, dork dorkdork. Dorkity dork, dork dork.
*grins*
--The Morrigan
P.S. Thanks for the email
woah didn't know I could leave comments for myself...
Morrigan, I'm pretty sure he meant he is the dork here. So don't worry, I'm still on the exciting level of genius of The Black Adder.
Greenberg: Actually I see your point, I wasn't asleep when I wrote it but I most certainly wasn't awake. I go the order reversed in the happy idiot one. As for termination, I'm assuming that there is a self-loop on death for model-checking purposes -- it's doesn't change the realism of the model unless we are modelling Jesus.
And yes, the way to live forever is to not die. I'm eternal. Didn't you know? (So far, at least.)
Post a Comment
<< Home