.Open Modal Logic . Introduction Modal logics were created so we can express ideas like the following without having to use quantifiers and variables: .Box For all time, at some time, never, ... For all future time, at some time in the past... X wants ... to be true. At all places.... In all possible worlds... In some worlds... It is impossible... In all subsystems.... As long as other subsystems don't do X this system will do Y. .Close.Box 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: .See http://portal.acm.org/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 ( .Hole )). A tabular form might also work well. .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 .See [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 .As_is []p one must write .As_is 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 .As_is 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: .See ./logic_8_Natural_Language.html#SUMO .See http://sigma.ontologyportal.org:4010/sigma/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. .Open Event-token reification for spatial-temporal modes Source .See http://plato.stanford.edu/entries/logic-temporal/ .Box Donald Davidson (1967). The problem is to give a formal account of the validity of such inferences as John saw Mary in London on Tuesday. Therefore, John saw Mary on Tuesday. The inference above is cast in logical form as for some e(See(John,Mary,e) & Place(e,London) & Time(e,Tuesday)), Therefore, for some e(See(John,Mary,e) & Time(e,Tuesday)). Also see the Event Calculus of Kowalski and Sergot (1986). .Close.Box 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: Jim saw John seeing Mary in London on Tuesday. for some e1,e2 (See(Jim, e1, e2) & See(John,Mary,e1) & Place(e1,London) & Time(e1,Tuesday)). Perhaps an axiom 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: for some e(Event(e, see, John, Mary) & Place(e, London) & Time(e, Tuesday)). This then permits statements at the meta level: for all x, Event(x, isa, see, verb). .Close.Net .Close The traditional presentation of a logic is to: .List Describe the syntax of the well formed formula. Describe the axioms and derivation rules. Present a semantic model using formal mathematics .Close.List . Sites Worth a visit Garson, James, "Modal Logic", The Stanford Encyclopedia of Philosophy (Winter 2001 Edition), Edward N. Zalta (ed.), URL = .See http://plato.stanford.edu/entries/logic-modal/ (philosophical but thorough). Animations of several logics with instructions in Dutch: .See http://plato.stanford.edu/entries/logic-modal/ (Easier to figure out than you might think...) .Open Simple Temporal Logics THe following are just to illustrate how I would approach constructing modalities within my MATHS system. The MATHS approach is: .List Define a syntax and semantics using MATHS. Derive useful and interesting properties and rules. .Close.List The following are some samples of modal propositional logics. . Simple Temporal Logic SIMPLE_TEMPORAL_LOGIC::=following, .Net We start with presuming that there is such a thing as Time: Time::Sets. We assume time is an ordered: |- $POSET(Time, strict=>before, strict_inverse=>after). We are interested in expressions that map Time into true and false values: P::=@^$Time. The propositions `P` are things that are true or false at particular times: .As_is `The sun is shining` .As_is `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 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: not:: P->P = map[p:P}(map[t:Time](not p(t)). .As_is not p is true at any time p is false and vice versa. and:: infix(P,P,P) = map[p,q:P](map[t:Time](p(t) and q(t) ), .As_is p and q at time t iff p is true at t and q is true at t. or:: infix(P,P,P) = map[p,q:P](map[t:Time](p(t) or q(t) ), .As_is p or q at time t iff either p is true at t or q is true at t. For p,q, if p then q ::= ((not p) or q ), .As_is At time t (if p then q is true) iff at time t( q is true or p is false). So, for example .As_is not(`It is raining` and `The sun is shining`). Then add the modal operator `everafter`: 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 .As_is everafter `sun shines in San Bernardino`. Define `sometime` as a modal operator: 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 .As_is sometime `it rains in Manchester`. We can rapidly show: (sometime, everafter, not)|-(T1): sometime = not everafter (not). (everafter, sometime)|- (T2):For p:@^Time, if everafter(p) then sometime(p). (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: 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. .Close.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. 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. |- (STL):$SIMPLE_TEMPORAL_LOGIC. next :: $Time---$Time. |- (discrte): for all t:Time, next(t) after t. For example to talk about the weather: .As_is tomorrow = next( today). We next introduce a modal operator that maps a temporal property one instance into the future: For p:$P, next_time(p) ::= map[t](p(next (t))). (next_time)|- next_time = map[p] (p o next). We can then show properties like ()|- (nn): not next_time = next_time not. ()|- (sn): sometime next_time = next_time sometime. ()|- (an): everafter next_time = next_time everafter. ()|- (ns): if next_time p then sometime p. ()|- (en): if ever_after p then next_time p. ()|- (nand): next_time(p and q) = (next_time p) and (next_time q). and so on... Can we show: sometime p = next_time p or sometime next_time p. everafter p = next_time p and everafter next_time p. Or do we need an induction axiom? .Hole .Close.Net SIMPLE_DISCRETE_TEMPORAL_LOGIC .Close Simple Temporal Logics .Open 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 .Table Name Symbol Example Meaning Pattern .Row and, or, not /\,\/,- p/\q $PC - .Row always [] []p For all future time p p,p,p,p,p,p... .Row sometime <> <>p At some future time p -p,-p,-p,-p,p,... .Row next () ()p In the next instant p -p,p,... .Row until U (p U q) q becomes true and before then p is always true. p,p,p,p,q,... .Close.Table . Details LTL::=following, .Net .Hole .Close.Net LTL . LTL in Practice .See [HavelunddLowryPenix01] .Close Linear Temporal Logic .Open 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. .Image CTL.gif [Trees of basic modalities of CTL] CTL::=following, .Net .See [HuthRyan00] . Syntax w::=wff, from $PC. Add the following operators. AX::w->w=`all next`. EX::w->w=`some next`. AG::w->w=`all possibilities forever`. EG::w->w=`some possibility forever`, There is a infinite path.... AF::w->w=`all possibilities sometime`. EF::w->w=`'some possibility sometime`. AU::w>w=`always until`, -- AU(p,q) requires `q` to be true at some time and `p` true at all previous times. AW::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. EU::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. MODEL::=Net{ States::@Sets. next::@(States, States). |-(nodeadstate): for all s:States( next(x)<>{} ). Wff::Propositions. label::States->Wff. For s:States, Paths(s) ::@#States={p:# $States. p[1]=s and for all (s,s'):p (s next s')}. satisfies::States><$wff>->@. satisfices::$wff->@States = map[p]{s:$States. $satisfies(s,p)}. |-satisfies(s, p) iff p in label(s). |-satisfies(s, not p) iff p not in label(s). |-satisfies(s, p and q) iff (p in label(s) and q in label(s)). |-satisfies(s, p or q) iff (p in label(s) or q in label(s)). |-satisfies(s, AX(p)) iff for all s':next(s)(satisfies(s',p)). |-satisfies(s, EX(p)) iff for some s':next(s)(satisfies(s',p)). |-satisfies(s, AG(p)) iff for all P:Paths(s)(P ==> satisfices(p)). |-satisfies(s, AF(p)) iff for all P:Paths(s)(P and satisfices(p)). |-satisfies(s, EG(p)) iff for some P:Paths(s)(P ==> satisfices(p)). |-satisfies(s, EF(p)) iff for some P:Paths(s)(P and satisfices(p)). |-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)). |-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)). AW(p, q)::=not EU( not q, (not p and not q)). }=::MODEL. . Text book notation .Table MATHS Text .Row and .Item .Image and.gif /\ .Row or .Item .Image or.gif \/ .Row not .Item .Image not.gif -| .Row AU(p,q) A[p U q] .Row EU(p,q) E[p U q] .Row 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 .See 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: .Table MATHS SMV .Row and & .Row or | .Row not ! .Row AU(p,q) A[p U q] .Row EU(p,q) E[p U q] .Close.Table . Properties Certain interesting and/or useful properties follow from the $MODEL. As a rule the future includes the present: if p then EF(p). if p then EG(p). Universallity implies existance if AG(p) then EG(p). if AF(p) then EF(p). if EG(p) then EF(p). ... Until X implies X at some time: AU(p,q) = AW(p, q) and AF(q). . Equivalences |- (dm1): not o AF = EG o not. |- (dm2): not o EF = AG o not. |- (dm3): not o AG = EF o not. |- (dm4): not o EG = AF o not. |- (dmx): not o EX = AX o not. |- (auaf): AF = AU( true, (_) ). |- (euef): AF = EU( false, (_) ). The following look like recursive or inductive definitions: |- (agx): AG = (_) and AX AG(_)). |- (egx): EG = (_) and EX EG(_)). |- (afx): AF = (_) or AX AF(_)). |- (efx): EF = (_) or EX EF(_)). |- (eux): EU = (2nd) or ((1st) and EX EU( (1st), (2nd) )) ). EU(p,q)= q or ( p and EX EU(p,q). |- (aux): AU = (2nd) or ((1st) and AX AU( (1st), (2nd) )) ). $TBD .Close.Net CTL . Practical Examples . Web sites PATTERNS::=http://www.cis.ksu.edu/santos/spec-patterns/ctl.html. .Close Computational Tree logic .Open 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 .See LichtensteinPnueli00 that describes the $PTL and proves lots of results both within $PTL and about $PTL. PTL::=Propositional_Temporal_Logic. Propositional_Temporal_Logic::=following, .Net wff::Syntax, well formed formula of the $PTL. |- $PROPOSITIONS(simple_proposition=>wff). next::wff->wff. prev0::wff->wff. until::infix(wff). since::infix(wff). prev::= not prev0 not. eventually::= true until (_). once::= true since (_). henceforth::= not eventually not. sofar::= not once not. p waitingfor q::=(henceforth p) or (p until q). p backto q::=(sofar p) or (p since q). p entails q::=henceforth(if p then q). p equiv q::=henceforth( p iff q). |-(F0):if henceforth p then p. |-(F1):next not p equiv not next p. |-(F2):next(if p then q)entails(if next p then next q). |-(F3):henceforth(if p then q)entails(if henceforth p then henceforth q). |-(F4):if henceforth p then henceforth next p. |-(F5):if p entails next p then p entails henceforth p. |-(F6): p until q equiv (q or (p and next (p until q))). |-(F7): p until q entails eventually q. |-(P1): prev p entails prev0 p. |-(P2): prev0(if p then q )entails if prev0 p then prev0 q. |-(P3): if henceforth p then henceforth prev0 p. |-(P4): (p since q)equiv(q or(p and prev(p since q)) ). |-(P5): prev0 false. |-(M8): p entails next prev0 p. all tautologies and inference rules in $PROPOSITIONS are inherited along with modus ponens. The original paper .See LichtensteinPnueli00 proves many theorems that hold in this logic. .Hole .Close.Net Propositional_Temporal_Logic PTL_MODEL::= following, .Net S::Sets. interpretation::=propositions->@S, the set of states in which (_) is true. computation::=Nat0 -> S. model::=computation>0 and (s,I,j-1) satisfies p). |- ( (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)). .Close.Net PTL_MODEL can show that $PTL is sound and complete for $PTL_MODEL. .Close Propositional Temporal Logic .Open Interval Logic INTERVAL_LOGIC::=Net{ .Source Hansen Ravn and Rischel 91 .See [HansenRavnRischel91]. Boolean expressions (predicates) are interpreted as describing the set of times when the formula are true. Hence interval functions and durations. Note: (a..b) = open interval ={x. a@. 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) duration_predicate(p) ::=\ceiling(p) ::= map[i](duration(p)(i)=length(i)>0) A;B::=map[i]for some m:i(true./A==>b..m and true./B==>m..e) eventually(A) ::=map[i](true;A;true), always(A) ::=not o eventually(A) o not. ... .Hole }=::INTERVAL_LOGIC. .Close Interval Logic . 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. .See [GargantiniMorzenti01] .See [Federetal94a] TRIO::=following .Net Time::@$Real. Normally would be the $Real numbers. Note: (a..b) = open interval ={x. a@,`Time dependent predicate`. For d:$Time, F:$TDP, Dist(F,d) :: $TBP= map[t]F(t+d). Dist(F,d) is true at time t if and only if F is true at time t+d. () |-(d1): for G:=Dist(F,d), all t, G(t)=F(t+d). ()|- (d2): Dist(F,d) = F((_) + d) = F o (_+d) = (_+d); F. Futr(F,d) ::= d>=0 and Dist(F,d). Past(F,d) ::= d>=0 and Dist(F, - d). Lasts(F,d) ::= for all d':(0..d) (Futr(F,d)). Lasted(F,d) ::= for all d':(0..d) (Past(F,d)). Alw(F) ::= for all d(Dist(F,d)). AlwF(F) ::= for all d, d>0(Dist(F,d)). AlwP(F) ::= for all d, d>0(Dist(F, -d)). () |- (a1): AlwF(F) = for all d, d>0(Futr(F,d)). Until(F,G) ::= for some t>0( Futr(G,t) and Lasts(F, t) ). Som(F) ::= for some d (Dist(F,d)). SomP(F) ::= for some d, d<0(Dist(F, d)). UpToNow(F) ::=for some d, d>0(Lasted(F,d)). NowOn(F) ::=for some d, d>0(Lasts(F,d)). Becomes(F) ::= UpToNow(not F) and (F or NowOn(F)), slightly different to Federeretal? LastTime(F,t) ::=Past(F,t) and Lasted(not F, t). NextTime(F,t) ::= Futr(F,t) and Lasts(not F, t). Can define closed and half closed versions of all the above! GargantiMorzenti also define some special types of predicates. Events are point based: they are true at a time but not before or after: Event::={F. Alw( if F then UpToNow(not F) and NowOn( not F))}. Interval_based_predicate ::= {F. Alw(if F then (UpToNow(F) or NowOn(F)) else UpToNow(not F) or NowOn(not F)))}. Note: if p then q else r = (if p then q) and (if not p then r). Left_Continuous_Interval_Based_Predicate ::={F. Alw((if F then UpToNow(F)else ` UpToNow(not F)))}. 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 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? Many results are claimed to be proved in GargantiMorzenti01. They go on to define time dependent variables and other ideas useful for analyzing requirements. .Close.Net TRIO .Open 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. .Hole ... .Close Kripke Semantics . Glossary TBD::="To Be Done". . References and Links PROPOSITIONS::=http://www.csci.csusb.edu/dick/maths/logic_10_PC_LPC.html#PROPOSITIONS. POSET::=http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Posets. RELATIONS::=http://www/dick/maths/logic_41_HomogenRelations.html LichtensteinPnueli00::=following, .See [LichtensteinPnueli00]. Real::=http://www.csci.csusb.edu/dick/maths/math_42_Numbers.html#Real_Numbers Search::=http://auto.search.msn.com/results.asp?FORM=AS14&v=1&RS=CHECKED&srch=4&q=Modal+logic. Sources::=http://groups.google.com/groups?q=temporal+logic&hl=en&selm=1993Jan27.140803.4254%40city.cs&rnum=1. .Close Modal Logic