Skip to main contentCal State San Bernardino
>> [CNS] >> [Comp Sci Dept] >> [R J Botting] >> [MATHS] >> logic_9_Modalities
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Jul 25 08:59:19 PDT 2006

Contents

    Modal Logic

      Introduction

       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.

      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, 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]

      The modalities based on the Propositional Calculus (PROPOSITION) 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....". 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. 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 

       		[]p
      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 apearance of a modal logic within the MATHS system.

      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 next subsection.

      Event-token reification for spatial-temporal modes

        Source [ http://plato.stanford.edu/entries/logic-temporal/ ]
          Donald Davidson (1967). The problem is to give a formal account of the validity of such inferences as
        1. John saw Mary in London on Tuesday.
        2. Therefore, John saw Mary on Tuesday.

          The inference above is cast in logical form as

        3. for some e(See(John,Mary,e) & Place(e,London) & Time(e,Tuesday)),
        4. Therefore, for some e(See(John,Mary,e) & Time(e,Tuesday)).

          Also see the Event Calculus of Kowalski and Sergot (1986).

        Partly Baked Ideas
        Net

          May be basis of Jackson's model of time as a series of alternating events and intervals with no events?

          Very flexible -- allows the same logic to handle many different temporal epistimologies by adjusting Time and Place.

          Also... event tokens could act as objects:

        1. Jim saw John seeing Mary in London on Tuesday.
        2. for some e1,e2 (See(Jim, e1, e2) & See(John,Mary,e1) & Place(e1,London) & Time(e1,Tuesday)). Perhaps an axiom
        3. for all e1,e2, p, t, See(Jim, e1, e2), See(John,Mary,e1) & Place(e1,p) & Time(e1,t)(Place(e2,p) & Time(e2,t)).

          Also compare Babel 17[Delaney] where events are given a verbal tag for future reference.

          The next level of generality is to reify the verbs:

        4. for some e(Event(e, see, John, Mary) & Place(e, London) & Time(e, Tuesday)).

          This then permits statements at the meta level:

        5. for all x, Event(x, isa, see, verb).

        (End of Net)

      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

      Sites Worth a visit

      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...)

      Simple Temporal Logics

        THe following are just to illustrate how I would approach constructing modalities within my MATHS system. 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,
        Net
          We start with presuming that there is such a thing as Time:
        1. Time::Sets.

          We assume time is an ordered:

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

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

        3. P::=@^Time.

          The propositions P are things 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
          p:=it is raining, and
        4. today:Time, then
          p(today) = today, it is raining.

          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 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 after this time, the proposition is always true. Note that unlike most modal operators, we do not induce the present as part of the future because we use the strict ordering 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 modallity:
          everafter sometime =(_) is true infinitely often, eternal recurrence.

          Also notice we have a spoeical modal implication:
          p being true everafter leads to q being true later. It behaves in this logic very like the normal if_then_ in PC or LPC. It is defined like this:

        14. 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.

        (End of Net SIMPLE_TEMPORAL_LOGIC)

        Simple Discrete Temporal Logic

        The SIMPLE_TEMPORAL_LOGIC makes view assumptions about the structure of time. If the time was discrete then it would consist of a series of instances. 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.
      2. SIMPLE_DISCRETE_TEMPORAL_LOGIC::=following,
        Net
          We start by importing all the formulae, assumptions, and theorems of the simple logic. Then we add assumptions that restrict time to being discrete.
        1. |- (STL): SIMPLE_TEMPORAL_LOGIC.
        2. next:: Time---Time.
        3. |- (discrte): for all t:Time, next(t) after t.

          For example to talk about the weather: 

           		tomorrow = next( today).

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

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

          We can then show properties like

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

          and so on...

          Can we show:

        12. sometime p = next_time p or sometime next_time p.
        13. everafter p = next_time p and everafter next_time p.

          Or do we need an induction axiom?

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


        (End of Net SIMPLE_DISCRETE_TEMPORAL_LOGIC)

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

      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 varifies that the Promela model of the system satisfies the requirement.

        Summary
        NameSymbolExampleMeaningPattern
        and, or, not/\,\/,-p/\qPC-
        always[][]pFor all future time pp,p,p,p,p,p...
        sometime<><>pAt some future time p-p,-p,-p,-p,p,...
        next()()pIn the next instant p-p,p,...
        untilU(p U q)q becomes true and before then p is always true.p,p,p,p,q,...

        Details
      1. LTL::=following,
        Net

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


        (End of Net LTL)

        LTL in Practice

         [HavelunddLowryPenix01]

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

      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.

        [Trees of basic modalities of CTL]

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

          Syntax
        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.
        5. EG::w->w=some possibility forever, There is a infinite path....
        6. AF::w->w=all possibilities sometime.
        7. EF::w->w='some possibility 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 iis (at some future time) then p must be true up until that time.
        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 labelling 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::=
          Net{
          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. satisfices::wff->@States = map[p]{s:States. satisfies(s,p)}.


          9. |-satisfies(s, p) iff p in label(s).
          10. |-satisfies(s, not p) iff p not in label(s).
          11. |-satisfies(s, p and q) iff (p in label(s) and q in label(s)).
          12. |-satisfies(s, p or q) iff (p in label(s) or q in label(s)).
          13. |-satisfies(s, AX(p)) iff for all s':next(s)(satisfies(s',p)).
          14. |-satisfies(s, EX(p)) iff for some s':next(s)(satisfies(s',p)).
          15. |-satisfies(s, AG(p)) iff for all P:Paths(s)(P ==> satisfices(p)).
          16. |-satisfies(s, AF(p)) iff for all P:Paths(s)(P and satisfices(p)).
          17. |-satisfies(s, EG(p)) iff for some P:Paths(s)(P ==> satisfices(p)).
          18. |-satisfies(s, EF(p)) iff for some P:Paths(s)(P and satisfices(p)).
          19. |-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)).
          20. |-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)).

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


          }=::MODEL.

          Text book notation

          MATHSText
          and /\
          or \/
          not -|
          AU(p,q)A[p U q]
          EU(p,q)E[p U q]
          AW(p,q)A[p W q]
          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:
          MATHSSMV
          and&
          or|
          not!
          AU(p,q)A[p U q]
          EU(p,q)E[p U q]

          Properties

          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).

          Universallity implies existance

        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).

          Equivalences


        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) )) ).

          TBD


        (End of Net CTL)

        Practical Examples

        Web sites

      2. 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,
        Net
        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,
        Net
        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::=
        Net{
          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]


        }=::INTERVAL_LOGIC.

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

      TRIO Temporal Logic

      Trio is a model logic that has been used to reason about complex time dependent properies of compterized 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
      Net
      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 predicte 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 formulae of modal logics. In normal logic we have a single domain of discourse. To model modes we envisage a collection of logical worlds. The worlds a connected and one knows about the connected ones. 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 model logic.

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

      1. ...

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

      Glossary

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

      References and Links
    3. PROPOSITIONS::= See http://www.csci.csusb.edu/dick/maths/logic_10_PC_LPC.html#PROPOSITIONS.

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

    5. RELATIONS::= See http://www.csci.csusb.edu/dick/maths/logic_41_HomogenRelations.html

    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, and give them a name. 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.

    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

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

End