here<\/a>.<\/p>\n The starting point for CTL is propositional logic. So we start with
\na basic propositional logic: a finite set of atomic statements (propositions)
\nthat we can use. (There are predicate extensions to CTL, but they make
\nit vastly more complicated, so we’ll stick to the simple, basic propositional
\nversion.) We can combine the propositions using the standard propositional
\nlogical operators – and, or, implication, and negation. <\/p>\n
Where it gets interesting is that we also have a set
\nof temporal quantifiers<\/em> which are used to specify the
\ntemporal properties of propositional statements. Every statement in
\nCTL has at least two temporal quantifiers. But before we get into them
\nin detail, we need to talk about the basic model of time in CTL.<\/p>\n The idea of the model CTL, as I said above, is based on Kripke
\nsemantics. Kripke semantics defines a changing system by using
\na collection of worlds. Each world consists of an assignment of truth
\nvalues to each of the basic propositions, and a set of
\nsuccessor worlds<\/em>. In Kripke semantics, you follow a path
\nthrough the worlds – in each step, you move from a
\nworld to one of its successors. In CTL, a world represents a moment in
\ntime; the successors to a world represent the possible moments of time
\nthat immediately follow it.<\/p>\n The Kripke semantics of CTL effectively gives us a
\nnon-deterministic<\/em> model of time. From a given moment, there can be
\nmore than one possible future – and we have
\nno way<\/em> of determining which possible future will come true
\nuntil we reach it. So time becomes a tree of possibilities – from each
\nmoment, you could go to any of its successors, so each moment spawns a
\nbranch for each of its successors – and each path through the tree represents
\na timeline for a possible future.<\/p>\n CTL gives us two different ways of talking about time in that tree
\nof possible futures; to make a meaningful temporal statement, we need
\nto combine them. First, if you look at time from any particular
\nmoment, there’s a collection of possible paths into the future – so
\nyou can talk about things in terms of the space of possible futures –
\nmaking statements that begin with things like “In all possible futures …”;
\nor “In some possible future …”. Second, you can talk about the steps
\nalong a particular path into the future – a sequence
\nof worlds that define one specific future. You can make statements
\nabout paths like “… will eventually be true”. By putting them
\ntogether, you can produce meaningful temporal statements:
\n“In all possible futures, X will always be true”; or
\n“In at least one possible future, X will eventually become true”.<\/p>\n
Following on this idea, there are two kinds of temporal
\nquantifiers<\/em> that are used to construct temporal
\nstatements: universe<\/em> quantifiers and path<\/em>
\nquantifiers. Every CTL statement uses a pair of quantifiers:
\none universe quantifier, and one path quantifier.<\/p>\n Universe quantifiers are used to make statements that range over
\nall paths forward from a particular moment in time. Path quantifiers
\nare used to make statements that range over all moments of time on a
\nparticular timeline-path. As I said above, in CTL statements, the
\nquantifiers always appear in pairs: one universe quantifier which
\nspecifies what set of potential futures you’re talking about, and one
\npath quantifier that describes the properties of paths within the set
\nquantified by the universe.<\/p>\n
There are two universe quantifiers, which correspond to the
\nuniversal and existential quantifiers from predicate logic. There’s
\n“A”, which is used to say that some statement is true in all
\npossible futures<\/em>; and there’s “E”, which is
\nused to say that there exists at least one possible future where
\nsomething is true.<\/p>\n Next, there are path quantifiers. Path quantifiers are similar to
\nuniverse quantifiers, except that instead of ranging over a set of
\npossible timelines, they range over the time-worlds on a specific
\ntimeline-path. There are five path quantifiers, which can
\nbe divided into three groups:<\/p>\n
\n- The simplest path quantifier is the immediate quantifier, X (next).
\nX is used to make a statement about the very next<\/em> time-world on this
\npath.<\/li>\n- There are universal and existential path quantifiers:
\n“G” (global), which is used to state a fact about every world-moment on the path,
\nand “F” (finally) which is used to state a fact about at
\nleast one world-moment along a particular timeline-path.<\/li>\n - There are temporal relationship quantifiers which are used to
\ndescribe relationships between facts. U(strong until) and W(weak
\nuntil). U and W both join statements, like “xUy” or “xWy”. What
\nthey mean is that the first statement (x) is true until<\/em>
\nthe second statement (y) becomes true. The strong form also means
\nthat the second statement must<\/em> eventually become true;
\nthe weak form says that x is true until y becomes true, but y may
\nnever become true – in which case x will be true forever.<\/li>\n<\/ol>\n It’s hard to see quite what all that means in the abstract,
\nbut once you see a few examples, it’s actually quite simple.<\/p>\n
\n-
AG.(I have a big nose)<\/code>: No matter what happens,
\nat every point in time, I will always have a big nose.<\/li>\n-
EF.(I lost my job)<\/code>: It’s possible that in some
\nfuture, I will be laid off. (Formally, there exists a possible
\ntimeline where the statement “I lost my job” will eventually
\nbecome true.<\/li>\n-
A.(I do my job well)W(I deserve to get fired)<\/code>: For
\nall possible futures, I do my job well until I deserve to be fired –
\nbut I won’t necessary eventually deserve to be fired – it’s possible (and
\nI hope very probable) that I’ll always do my job well, and so “I deserve to be fired”
\nwill never become true.<\/li>\n-
A.(I am alive)U(I am dead)<\/code>: No matter what happens, I
\nwill be alive until I die – and my eventual death is absolutely inevitable.<\/li>\n-
AG.(EF.(I am sick))<\/code>: It’s always possible that I’ll eventually get sick.<\/li>\n-
AG.(EF.(My house is painted blue) ∨ AG.(My house is painted brown))<\/code>: In
\nall possible futures, either my house will eventually be painted blue, or it will stay
\nbrown. It will never be any color other than blue or brown.<\/li>\n<\/ul>\nWhat’s it good for?<\/h3>\n
Up above, I said that CTL, despite its simplicity, is actually very
\nuseful. What’s it really good for?<\/p>\n
I’m not going to go into detail – but one of the main uses of it
\nis in something called model checking<\/em>. Model checking is a
\ntechnique used by both hardware and software engineers to check the
\ncorrectness of certain temporal aspects of their system. They write a
\nspecification of their system in terms of CTL; and then they use an
\nautomated tool that compares an actual implementation of a piece of
\nhardware or software to the specification. The system can then verify
\nwhether or not the system does what it’s supposed to; and if not, it
\ncan provide a specific counter-example demonstrating when it will
\ndo the wrong thing.<\/p>\n In hardware model checking, you’ve got a simple piece of hardware
\n– like a single functional unit from a microprocessor. That hardware
\nis, basically, a complex finite state machine. The way that you can think of
\nit is that the hardware has some set of points where it can have a
\nzero or a one. Each of those points can be represented by a
\nproposition. Then you can describe operations in terms of how outputs
\nare produced from inputs.<\/p>\n
So, for example, if you were looking at a functional unit that
\nimplements division, one of the propositions would be “The divide by
\nzero flag is set”. Then your specification would include statements
\nlike AG.(DivisorIsZero)&implies;AF.(DivideByZeroFlag)<\/code>. That
\nspecification says that if the divisor is zero, then eventually
\nthe divide by zero flag will be set. It does not<\/em> specify
\nhow long it will take – it could take one step, or it could take 100. But
\nsince the behavior that we care about with that specification should
\nbe true regardless of the details of how the divider is implemented,
\nwe don’t want to specify how many steps – the important behavior is that
\nif you try to divide by zero, the appropriate flag bit is set.<\/p>\n Obviously, the real specifications are a lot more complex than that,
\nbut that gives you the general sense.<\/p>\n
It’s also used in software. A friend of mine from when I worked at
\nIBM did some really cool work on model-checking software. Lots of people
\nhave looked at that, but it doesn’t appear to be too useful in general –
\nwriting the specifications is hard, and checking them given the amount
\nof state in a typical program is a nightmare. What my friend did is
\nrealize that when you look at a multithreaded system, the desired
\nsynchronization behavior is generally pretty simple – and is almost
\nideally suited for description in a language like CTL. So he worked
\nout a way of using model checking to verify the correctness of
\nthe synchronization behaviors of software systems. <\/p>\n
So that’s the basics of CTL – an extremely simple, but extremely
\nuseful logic for describing time-based behaviors.<\/p>\n","protected":false},"excerpt":{"rendered":"
This post is something that I’m thinking of including in my book. I haven’t decided whether I want to spend this much time on logics; they’re really interesting and fun – but there’s lots of other interesting and fun stuff, and there’s only so much space. The topic of the moment is temporal logic – […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[10,33],"tags":[],"class_list":["post-768","post","type-post","status-publish","format-standard","hentry","category-book","category-logic"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-co","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/768","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=768"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/768\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=768"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=768"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=768"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}