[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_9_Modalities
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Feb 28 07:45:17 PST 2011


    Modal Logic


      Modal logics were created so we can express ideas like the following without having to use quantifiers and variables:
      1. For all time, at some time, never, ...
      2. For all future time, at some time in the past...
      3. X wants ... to be true.
      4. At all places....
      5. In all possible worlds...
      6. In some worlds...
      7. It is impossible...
      8. In all subsystems....
      9. As long as other subsystems don't do X this system will do Y.

      These ideas are called modes. There are a large number of logics that attempt to model them.

      They date back to Aristotle (of course). These early thinkers rapidly realized that the meaning of "at some time, the sky will fall" depends on whether the future is pre-determined or full of possibilities. The different models of time and different modes of expression came under intense formal study in the twentieth century for three reasons: (1) to find a logic where "if _ then _" behaved more intuitively, (2) because the modal system were there, and (3) because they looked as if they might be useful in thinking about complex computerized systems.

      My interest is in computerized systems so these notes have some examples of modal logics designed to talk about their behavior. When computerizing complex high risk situations we need to be very clear about what we are asking for. If we want the system to exhibit some property in every possible state, and for all time, then we don't want it merely, at all time, to have the option of fulfilling the property sometimes. English is not very good at expressing such distinctions. Studying modal logics uncovers the half-a-dozen different ways we may want a piece of software to have a property. Some modal logics make it easy to calculate whether the logical behavior of a piece of software (a model) satisfies its requirements.

      Notice that it is useful to be able to reason about time varying properties of complex computerized systems. Indeed checking that software fits such properties has uncovered some difficult to find bugs in real software. However the normal notation is somewhat clumsy and so there has been research on graphic notations ( GIL: [ citation.cfm?id=192218.192226&coll=portal&dl=ACM&idx=J790&part=transaction&WantType=transaction&title=ACM%20Transactions%20on%20Software%20Engineering%20and%20Methodology%20%28TOSEM%29&CFID=1643654&CFTOKEN=8691090 ] and Buchi automata ( [click here [socket symbol] if you can fill this hole] )). A tabular form might also work well. [click here [socket symbol] if you can fill this hole]

      Philosophers are interested in Modal Logics because they are not well understand, and indeed have interesting problems. The modalities based on the Propositional Calculus (see PROPOSITION below) are not problematic. For example you can get a simple extension that lets you talk about "all possibly computations" without having to have any quantified variables: "for all x....".

      But when quantifiers and equality are introduced as well as modalities, some interesting things can occur. In particular there is a loss of referential transparency: you can no longer substitute equals for equals. Euclid can not be trusted with hopes, wants, and beliefs. For example in the mode of "wanting things to be true": Hamlet may want the person behind curtains dead, but he does not want Polonius to die, even though Polonius is the person hiding behind the curtains.

      Another bad effect of combining modes and quantifiers is that some expressions become ambiguous [FittingMendelsohn98] because modes have no explicit scope or variables. The standard MATHS notation has predicates and quantifiers and so the standard approach to modes in the MATHS notation is to treat them explicitly as quantifiers. This sacrifices simplicity on the altar of accuracy. Thus instead of being able to write

      one must write
       		for all t:Time(p(t)).
      This is longer but more precise. The precision is only important if p(t) includes other variables and quantifiers. However MATHS permits operators to operate on predicates like p above as well as on Boolean propositions so we could define
       		For P:Time->@, always(P) ::= for all t:Time(P(t)).
      and get the appearance of a modal logic within the MATHS system. I will demonstrate this below -- see SIMPLE_TEMPORAL_LOGIC for details.

      Michael Jackson's recent work has another approach for mapping temporal modes into the lower predicate calculus. This seems to be the approach taken to modeling time in the SUMO ontology: [ logic_8_Natural_Language.html#SUMO ] [ Browse.jsp?kb=SUMO&term=time ]

      This approach has been taken further by introducing a token that identifies events which links them to Places and Times, see [ Event-token reification for spatial-temporal modes ] below

      Sites Worth a visit for the traditional approach to Modal Logic

      The traditional presentation of a logic is to:
      1. Describe the syntax of the well formed formula.
      2. Describe the axioms and derivation rules.
      3. Present a semantic model using formal mathematics

      Garson, James, "Modal Logic", The Stanford Encyclopedia of Philosophy (Winter 2001 Edition), Edward N. Zalta?(ed.), URL = <http://plato.stanford.edu/archives/win2001/entries/logic-modal/> [ http://plato.stanford.edu/entries/logic-modal/ ] (philosophical but thorough).

      Animations of several logics with instructions in Dutch: [ http://plato.stanford.edu/entries/logic-modal/ ] (Easier to figure out than you might think...)

      The Wikipedia [ Modal_logic ] is pretty reliable on Modal logic.

      Any more? [click here [socket symbol] if you can fill this hole]

      Simple Temporal Logics

        The following are just to illustrate how I would approach constructing modalities within my MATHS system.
          They are not in the standard MATHS rules, but you can include them in your work by using
           .See http://csci.csusb.edu/dick/maths/logic_9_Modalities.html#SIMPLE_TEMPORAL_LOGIC
          for example

        The MATHS approach is:
        1. Define a syntax and semantics using MATHS.
        2. Derive useful and interesting properties and rules.

        The following are some samples of modal propositional logics.

        Simple Temporal Logic

      1. SIMPLE_TEMPORAL_LOGIC::=following,
          We start with presuming that there is such a thing as Time. Ot to be precise that there is a set of times we can call "Time".
        1. Time::Sets=given.

          We assume time is an ordered:

        2. |-POSET(Time, strict=>before, inverse=>after).

          Note. Sun Feb 27 10:47:13 PST 2011. I have just changed the above assertion so that after is no longer the strict_inverse of before. This means that for all Time t is t after t. Also for no Time t is t before t.

        3. (-1)|-t after t.

          We are interested in expressions that map Time into true and false values:

        4. P::=@^Time.

          The propositions P are statements that are true or false at particular times:

           		`The sun is shining`
           		`It is raining`.
          If we supply a time then we assume that we can be sure that a proposition is either true or false at that time. So, suppose
          1. p:=it is raining, and
          2. today:Time, then
          3. p(today) = today it is raining.

          (End of Net)

          Note. The above presumes that we can be definite about the state of our propositions at any given time. Other temporal logics do not make this assumption.

          We can define Boolean operations on such propositions:

        5. not:: P->P = map[p:P}(map[t:Time](not p(t)).
           		not p is true at any time p is false and vice versa.
        6. and:: infix(P,P,P) = map[p,q:P](map[t:Time](p(t) and q(t) ),
           		p and q at time t iff p is true at t and q is true at t.
        7. or:: infix(P,P,P) = map[p,q:P](map[t:Time](p(t) or q(t) ),
           		p or q at time t iff either p is true at t or q is true at t.
        8. For p,q, if p then q::= ((not p) or q ),
           		At time t ((if p then q is true) iff ( q is true or p is false) ).
           		At time t (if p then q is true) iff at time t( q is true or p is false).

          So, for example

           	not(`It is raining` and `The sun is shining`).

          Then add the modal operator everafter:

        9. everafter:: P->P= for all Time t where t after (_) ( p(t) ), that indicates that the proposition is always true, now and for ever after.

          For example

           		everafter `sun shines in San Bernardino`.

          Define sometime as a modal operator:

        10. sometime:: P->P= for some Time t where t after (_) ( p(t) ), indicating that at some time now or later the proposition is true.

          For example

           		sometime `it rains in Manchester`.

          We can rapidly show:

        11. (sometime, everafter, not)|- (T1): sometime = not everafter (not).
        12. (everafter, sometime)|- (T2): For p:@^Time, if everafter(p) then sometime(p).
        13. (everafter, sometime)|- (T3): If p=Time+>true then everafter p and sometime p.

          Notice this intuitive interpretation of the combined modality:

        14. everafter sometime =(_) is true infinitely often, eternal recurrence.

          Also notice we have a special modal implication:

        15. p being true everafter leads to q being true later.

          This behaves in like the normal if_then_ in PC or LPC. It is defined like this:

        16. For p,q:P, p~~>q::P = everafter( if p then sometime q), at any time, if p is true then at some time after that q will be true. So, for example, if p is true now and p~~>q, then, sometime (soon?) q will be true.

        (End of Net SIMPLE_TEMPORAL_LOGIC)

        Simple Discrete Temporal Logic

        The SIMPLE_TEMPORAL_LOGIC makes few assumptions about the structure of time. Here I introduce the assumption that time is a sequence of discrete instants, one, after another, and with every instant just before the next one. Each time would be followed by another time. Hence we can talk about a property being true in the next instant as well as for all time or at some future time.
          We start by importing all the formulas, assumptions, and theorems of the simple logic. Then we add assumptions that restrict time to being discrete.
        1. |- (STL): SIMPLE_TEMPORAL_LOGIC. (Includes the previous logic here).
        2. next:: Time---Time, maps one Time into a unique next Time, and each Time t1 has a single previous Time t2 such that t1 = next t2.

        3. |- (discrete): for all t1,t2:Time, t1 after t2 iff t1 = next^(0..*) t2.

        4. (-1)|- (STL0): next(t) after t.

          I could use the 'prime' notation:

        5. For all Time t, t' ::= next(t).

          For example to talk about the weather:

           		tomorrow =  today'.

          We introduce a modal operator next_time that maps a temporal property one instance into the future:

        6. For p:P, next_time(p)::= map[t](p(next (t))).
        7. (next_time)|-next_time = map[p] (p o next).

          We can then show properties like

        8. (above)|- (nn): not next_time = next_time not.
        9. (above)|- (sn): sometime next_time = next_time sometime.
        10. (above)|- (an): everafter next_time = next_time everafter.
        11. (above)|- (ns): if next_time p then sometime p.
        12. (above)|- (en): if ever_after p then next_time p.
        13. (above)|- (nand): next_time(p and q) = (next_time p) and (next_time q).

          To take this further we would add a special Time 0, with the properties

        14. For all t, t after 0, and
        15. For no t, t before 0.

          So that

        16. sometime p = p(0) or sometime next_time p,
        17. everafter p = p(0) and everafter next_time p.


      . . . . . . . . . ( end of section Simple Temporal Logics) <<Contents | End>>

      LTL - Linear Temporal Logic

        Linear temporal logic( LTL ) is a popular language for verifying properties of complex safety-critical systems. It can be used as part of the SPIN tool to describe requirements. A language called Promela is used to describe how the system evolves. SPIN verifies that the Promela model of the system satisfies the requirement.

        LTL expressions express constraints or properties of infinite sequences called paths. An expression applies to a set sequences if and only if it applies to the whole sequence.


        propertyp,q,rptrue at start of sequencep,?,?,?,...
        and, or, not/\,\/,-p/\qPC-
        alwaysG,[][]pFor all future time pp,p,p,p,p,p...
        sometimeF, <><>pAt some future time p-p,-p,-p,-p,p,...
        nextX, ()()pIn the next instant p?,p,...
        untilU(p U q)q becomes true and before then p is always true.p,p,p,p,q,...
        weak untilW(p W q)p is always true or at least until q is true.
        releaseR(p R q)= not(not p U not q)

        (Close Table)

        LTL Details

        See [ Linear_temporal_logic ] on the Wikipedia

        LTL in Practice


      . . . . . . . . . ( end of section Linear Temporal Logic) <<Contents | End>>

      CTL - Computational Tree logic

        This is a popular logic for proving properties of non-deterministic concurrent programs and circuits. It assumes time is discrete: each state is followed by anther state at the next interval of time. It does not assume that each state is followed by a only one state. Thus, suppose that the current state can be followed by states a, b, and c and that p is true in all of these states, but q is true in only state b then we can assert that AX p(all next) and EX q(exists next). We can not assert AX q since q is not true in All neXt states. Here is an informal picture of the semantics of CTL, followed by a more formal presentation.

        Here is a graphic summary: Black nodes are where p is true, white nodes where it is false and grey nodes where we don't care.

        [Trees of basic modalities of CTL]

      1. CTL::=following,
          Source [HuthRyan00]


        1. w::=wff, from PC. Add the following operators.
        2. AX::w->w=all next.
        3. EX::w->w=some next.

        4. AG::w->w=all possibilities forever, on all paths....
        5. EG::w->w=some possibility forever, there is an infinite path....
        6. AF::w->w=all possibilities sometime, what ever path there comes a time when....
        7. EF::w->w='some possibility sometime, it is possible that it beomes true on some path sometime...
        8. AU::w><w->w=always until, -- AU(p,q) requires q to be true at some time and p true at all previous times.
        9. AW::w><w->w=weak always until, -- does not require q to be true, but if it is (at some future time) then p must be true up until that time, and if q is never true, then p must be true for ever. (Thanks to Alejandro Hernandez who sent me note1 below)
        10. EU::w><w->w=sometime until.

          Semantic Model

          The semantics is in terms of a model M and a state s of that model. The Model M has states, a next relationship, and a labeling relation that maps states into sets of propositions. This is used to define satisfaction: that in the model, starting at the state, the formula is true.
        11. MODEL::=
          1. States::@Sets.
          2. next::@(States, States).
          3. |- (nodeadstate): for all s:States( next(x)<>{} ).
          4. Wff::Propositions.
          5. label::States->Wff.

          6. For s:States, Paths(s)::@#States={p:# States. p[1]=s and for all (s,s'):p (s next s')}.

          7. satisfies::States><wff>->@.
          8. satisfies(someState, someFormula) ∈ {false, true}. satisfices::wff->@States = map[p]{s:States. satisfies(s,p)}.
          9. satisfices(someFormula) = for each wff p, the set of states s where s satisfies p

          10. |-satisfies(s, p) iff p in label(s).
          11. |-satisfies(s, not p) iff p not in label(s).
          12. |-satisfies(s, p and q) iff (p in label(s) and q in label(s)).
          13. |-satisfies(s, p or q) iff (p in label(s) or q in label(s)).
          14. |-satisfies(s, AX(p)) iff for all s':next(s)(satisfies(s',p)).
          15. |-satisfies(s, EX(p)) iff for some s':next(s)(satisfies(s',p)).
          16. |-satisfies(s, AG(p)) iff for all P:Paths(s)(P ==> satisfices(p)).
          17. |-satisfies(s, AF(p)) iff for all P:Paths(s)(P and satisfies(p)).
          18. |-satisfies(s, EG(p)) iff for some P:Paths(s)(P ==> satisfices(p)).
          19. |-satisfies(s, EF(p)) iff for some P:Paths(s)(P and satisfies(p)).
          20. |-satisfies(s, AU(p,q)) iff for all P:Paths(s), some i:1..#P-1(satisfies(P[i+1], q) and P[1..i] ==> satisfices(p)).
          21. |-satisfies(s, EU(p,q)) iff for some P:Paths(s), some i:1..#P-1(satisfies(P[i+1], q) and P[1..i] ==> satisfices(p)).

          22. AW(p, q)::=not EU( not q, (not p and not q)).


          Text book notation

          and /\
          or \/
          not -|
          AU(p,q)A[p U q]
          EU(p,q)E[p U q]
          AW(p,q)A[p W q]

          (Close Table)
          Note. The GIFs of the logic symbols above were downloaded from Michael Huths excellent web site at [ http://www.cis.ksu.edu/~huth/lics/ ] for the "Logic in Computer Science" text book authored with Mark Ryan.

          SMV notation

          The Simple Model Verifier (SMV) has a different notation:
          AU(p,q)A[p U q]
          EU(p,q)E[p U q]

          (Close Table)


          Certain interesting and/or useful properties follow from the MODEL.

          As a rule the future includes the present:

        12. if p then EF(p).
        13. if p then EG(p).

          Universality implies existence

        14. if AG(p) then EG(p).
        15. if AF(p) then EF(p).
        16. if EG(p) then EF(p).
        17. ...

          Until X implies X at some time:

        18. AU(p,q) = AW(p, q) and AF(q).


        19. |- (dm1): not o AF = EG o not.
        20. |- (dm2): not o EF = AG o not.
        21. |- (dm3): not o AG = EF o not.
        22. |- (dm4): not o EG = AF o not.
        23. |- (dmx): not o EX = AX o not.

        24. |- (auaf): AF = AU( true, (_) ).
        25. |- (euef): AF = EU( false, (_) ).

          The following look like recursive or inductive definitions:

        26. |- (agx): AG = (_) and AX AG(_)).
        27. |- (egx): EG = (_) and EX EG(_)).
        28. |- (afx): AF = (_) or AX AF(_)).
        29. |- (efx): EF = (_) or EX EF(_)).
        30. |- (eux): EU = (2nd) or ((1st) and EX EU( (1st), (2nd) )) ).
        31. EU(p,q)= q or ( p and EX EU(p,q).
        32. |- (aux): AU = (2nd) or ((1st) and AX AU( (1st), (2nd) )) ).


        (End of Net CTL)

        Similar second order predicates are defined in [ logic_41_HomogenRelations.html#Paths and Trajectories ] and [ maths/math_71_Auto...Systems.html#Discrete_Dynamic_System ] o this site.

        Practical Examples

        Any suggestions? [click here [socket symbol] CTL in Practice if you can fill this hole]

        Web sites

      2. CTL_PATTERNS::= See http://www.cis.ksu.edu/santos/spec-patterns/ctl.html.

      . . . . . . . . . ( end of section Computational Tree logic) <<Contents | End>>

      Propositional Temporal Logic

        The following comes from a paper that summarizes the conclusions of 20 years research into a modal logic for talking about step-by-step computations [ LichtensteinPnueli00 ] that describes the PTL and proves lots of results both within PTL and about PTL.

      1. PTL::=Propositional_Temporal_Logic.
      2. Propositional_Temporal_Logic::=following,
        1. wff::Syntax, well formed formula of the PTL.
        2. |-PROPOSITIONS(simple_proposition=>wff).
        3. next::wff->wff.
        4. prev0::wff->wff.
        5. until::infix(wff).
        6. since::infix(wff).
        7. prev::= not prev0 not.
        8. eventually::= true until (_).
        9. once::= true since (_).
        10. henceforth::= not eventually not.
        11. sofar::= not once not.
        12. p waitingfor q::=(henceforth p) or (p until q).
        13. p backto q::=(sofar p) or (p since q).
        14. p entails q::=henceforth(if p then q).

        15. p equiv q::=henceforth( p iff q).

        16. |- (F0): if henceforth p then p.
        17. |- (F1): next not p equiv not next p.
        18. |- (F2): next(if p then q)entails(if next p then next q).
        19. |- (F3): henceforth(if p then q)entails(if henceforth p then henceforth q).
        20. |- (F4): if henceforth p then henceforth next p.
        21. |- (F5): if p entails next p then p entails henceforth p.
        22. |- (F6): p until q equiv (q or (p and next (p until q))).
        23. |- (F7): p until q entails eventually q.

        24. |- (P1): prev p entails prev0 p.
        25. |- (P2): prev0(if p then q )entails if prev0 p then prev0 q.
        26. |- (P3): if henceforth p then henceforth prev0 p.
        27. |- (P4): (p since q)equiv(q or(p and prev(p since q)) ).
        28. |- (P5): prev0 false.

        29. |- (M8): p entails next prev0 p.

          all tautologies and inference rules in PROPOSITIONS are inherited along with modus ponens.

          The original paper [ LichtensteinPnueli00 ] proves many theorems that hold in this logic. [click here [socket symbol] if you can fill this hole]

        (End of Net Propositional_Temporal_Logic)

      3. PTL_MODEL::= following,
        1. S::Sets.
        2. interpretation::=propositions->@S, the set of states in which (_) is true.
        3. computation::=Nat0 -> S.
        4. model::=computation><interpretation.
        5. triple::=computation><interpretation><Nat0.
        6. satisfies::@(triple,wff).
        7. |-( (s,I,j) satisfies true) and not ( (s,I,j) satisfies false).

        8. |-for P:proposition( (s,I,j) satisfies P iff s[] in I(P)).
        9. ...
        10. |-( (s,I,j) satisfies p until q) iff for some k:j.. ((s,I,k) satisfies q and for all i:j..k-1 ((s,I,i) satisfies p)).

        11. |-( (s,I,j) satisfies next p) iff (s,I,j+1) satisfies p).

        12. |-( (s,I,j) satisfies prev0 p) iff j=0 or j>0 and (s,I,j-1) satisfies p).
        13. |-( (s,I,j) satisfies p since q) iff for some k:0..j ((s,I,k) satisfies q and for all i:k+1..j ((s,I,i) satisfies p)).

        (End of Net PTL_MODEL)

        can show that PTL is sound and complete for PTL_MODEL.

      . . . . . . . . . ( end of section Propositional Temporal Logic) <<Contents | End>>

      Interval Logic

      1. INTERVAL_LOGIC::=

          Source: Hansen Ravn and Rischel 91 [HansenRavnRischel91].

          Boolean expressions (predicates) are interpreted as describing the set of times when the formula are true. Hence interval functions and durations.

        1. Note: (a..b) = open interval ={x. a<x<b},
        2. a..b=closed interval={x. a<=x<=b},
        3. [a..b)=half open interval={x. a<=x<b},
        4. (a..b]=half open interval={x. a<x<=b},

        5. Times::= Real.

          Interval functions

        6. intervals::=Times)->@. duration(p)(b..e) ::=measure{x:b..e||p}, or equiv integral(x,b,e,if(p,1,0)). length(b..e)=b-e=duration(x in b..e)
        7. duration_predicate(p)::=\ceiling(p) ::=
        8. map[i](duration(p)(i)=length(i)>0)
        9. A;B::=map[i]for some m:i(true./A==>b..m and true./B==>m..e)
        10. eventually(A)::=map[i](true;A;true),
        11. always(A)::=not o eventually(A) o not.

          ... [click here [socket symbol] if you can fill this hole]


      . . . . . . . . . ( end of section Interval Logic) <<Contents | End>>

      TRIO Temporal Logic

      Trio is a modal logic that has been used to reason about complex time dependent properties of computerized system. It has a large number of modes corresponding to tenses. All derived form one simple one by using quantification over time. [GargantiniMorzenti01] [Federetal94a]
    1. TRIO::=following
      1. Time::@Real. Normally would be the Real numbers. Note: (a..b) = open interval ={x. a<x<b}, a..b=closed interval={x. a<=x<=b), [a,b), ... [ Intervals in math_42_Numbers ]

      2. |-GROUP(Time, +, -, 0). Implicitly assumes times are closed under addition.
      3. TDP::= Time->@,Time dependent predicate.
      4. For d:Time, F:TDP, Dist(F,d):: TBP= map[t]F(t+d).
      5. Dist(F,d) is true at time t if and only if F is true at time t+d.
      6. ()|- (d1): for G:=Dist(F,d), all t, G(t)=F(t+d).
      7. (above)|- (d2): Dist(F,d) = F((_) + d) = F o (_+d) = (_+d); F.
      8. Futr(F,d)::= d>=0 and Dist(F,d).
      9. Past(F,d)::= d>=0 and Dist(F, - d).
      10. Lasts(F,d)::= for all d':(0..d) (Futr(F,d)).
      11. Lasted(F,d)::= for all d':(0..d) (Past(F,d)).
      12. Alw(F)::= for all d(Dist(F,d)).
      13. AlwF(F)::= for all d, d>0(Dist(F,d)).
      14. AlwP(F)::= for all d, d>0(Dist(F, -d)).
      15. ()|- (a1): AlwF(F) = for all d, d>0(Futr(F,d)).
      16. Until(F,G)::= for some t>0( Futr(G,t) and Lasts(F, t) ).
      17. Som(F)::= for some d (Dist(F,d)).
      18. SomP(F)::= for some d, d<0(Dist(F, d)).
      19. UpToNow(F)::=for some d, d>0(Lasted(F,d)).
      20. NowOn(F)::=for some d, d>0(Lasts(F,d)).
      21. Becomes(F)::= UpToNow(not F) and (F or NowOn(F)), slightly different to Federeretal?
      22. LastTime(F,t)::=Past(F,t) and Lasted(not F, t).
      23. NextTime(F,t)::= Futr(F,t) and Lasts(not F, t).

      24. Can define closed and half closed versions of all the above!

        GargantiMorzenti also define some special types of predicates.

      25. Events are point based: they are true at a time but not before or after:
      26. Event::={F. Alw( if F then UpToNow(not F) and NowOn( not F))}.
      27. Interval_based_predicate::= {F. Alw(if F then (UpToNow(F) or NowOn(F)) else UpToNow(not F) or NowOn(not F)))}.
      28. Note: if p then q else r = (if p then q) and (if not p then r).
      29. Left_Continuous_Interval_Based_Predicate::={F. Alw((if F then UpToNow(F)else ` UpToNow(not F)))}.
      30. Right_Continuous_Interval_Based_Predicate::={F. Alw((if F then NoOn(F) else UpToOn(not F)))}.

        Some TDP are more likely to exist in real systems, and about which properties are easier to prove. For example a predicate Z defined by Past(Z, t) iff for some n:1..(t=1/n) describes an event defined to occur at an infinite number of times 1, 1/2, 1/3, ... in the near past. Non-Zeno predicates are

      31. nonZeno(F)::@ TDP = Alw( (UpToNow(not F) or UpToNow(F)) and (NowOn(not F) or NowOn(F) ).

        Note --the idea of a nonZeno predicate allows events to occur infinitely close to each other but excludes events that happen an infinite number of times.

        Question: What about switch bounces?

      32. Many results are claimed to be proved in GargantiMorzenti01.
      33. They go on to define time dependent variables and other ideas useful for analyzing requirements.

      (End of Net TRIO)

      Kripke Semantics

        Kripke semantics provides a uniform way to interpret the formulas of modal logics. In normal logic we have a single domain of discourse. To model modes we envisage a collection of worlds, each with its own logic. These worlds are connected and one knows about the connected ones but not the others. One mode is in all connected words and the other is modeled by in some connected world. By assuming various properties of the connection relationship we can create a model of any well-known modal logic.

        [click here [socket symbol] Kripke Semantics if you can fill this hole]

      . . . . . . . . . ( end of section Kripke Semantics) <<Contents | End>>


          Hello, my name is Alejandro Hernandez, I am a research assistant at DTU, Denmark. I have found an omission in your site about Modal Logic , in the CTL section. In the informal explanation of the Always Weak Until operator (AW) you say "does not require q to be true, but if it is (at some future time) then p must be true up until that time", but there it is not clear the "if not" part, which it is that p should be true always (because q never will be). I spent a while trying to understand that (and realizing that the formal definition in terms of the the negation of the Sometimes Until did not fit the informal explanation), until I found another site where it is more clear. I just wanted to tell you so if you fix it then the next person will not spend the time I did. Sorry, and thank you very much for all that I have learned reading your site!


      1. TBD::="To Be Done".

        References and Links

      2. PROPOSITIONS::= See http://www.csci.csusb.edu/dick/maths/logic_10_PC_LPC.html#PROPOSITIONS.

      3. POSET::= See http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Posets.

      4. RELATIONS::= See http://cse.csusb.edu/dick/maths/logic_41_HomogenRelations.html

      5. GargantiMorzenti01::=following, [GargantiMorzenti01].

      6. LichtensteinPnueli00::=following, [LichtensteinPnueli00].

      7. Real::= See http://www.csci.csusb.edu/dick/maths/math_42_Numbers.html#Real_Numbers
      8. Search::= See http://auto.search.msn.com/results.asp?FORM=AS14&v=1&RS=CHECKED&srch=4&q=Modal+logic.
      9. Sources::= See http://groups.google.com/groups?q=temporal+logic&hl=en&selm=1993Jan27.140803.4254%40city.cs&rnum=1.

      . . . . . . . . . ( end of section Modal Logic) <<Contents | End>>

      Notes on MATHS Notation

      Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

      Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

      The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

      For a complete listing of pages in this part of my site by topic see [ home.html ]

      Notes on the Underlying Logic of MATHS

      The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

      For a more rigorous description of the standard notations see

    2. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html


    3. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
    4. given::reason="I've been told that...", used to describe a problem.
    5. given::variable="I'll be given a value or object like this...", used to describe a problem.
    6. goal::theorem="The result I'm trying to prove right now".
    7. goal::variable="The value or object I'm trying to find or construct".
    8. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
    9. hyp::reason="I assumed this in my last Let/Case/Po/...".
    10. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
    11. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
    12. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.