What is temporal logic. Examples of determination of TL. Applications TL. Using predicates. Temporal analysis of natural language

Temporal logic:

Adds temporal operators

Describe how static conditions change over time

Two main ways to represent temporal logic:

Linear time: describes single possible time line

LTL (Linear Temporal Logic): Spin

Branching time: describes all possible time lines

CTL (Computation Tree Logic)

Using

} Use to describe system behavior

◦ Describes actions of system

◦ In terms of state sequences

} Use temporal logic to describe property of state sequences

} Use model checker to verify TL property

◦ Checks TL property against automation

◦ Exhaustively checks the automation

◦ Automatic checking

Basic idea

} Truth changes over time

} Must say when things are true,

◦ Not just what is true

4 basic operators:

◦ [ ] : always

◦ <> : sometime or eventually

◦ X : next time or next step

◦ U : until

"If the message m will arrive at the entrance to the channel, then sometime in the future it will output“

Modality- a category that defines the relationship to reality

Modal Logic- any formal logical system, in which there are modal operators

} M - "it is possible that" (Mp - "it is possible that p" )

} L - "requires that" (Lq - "q necessarily satisfied") n

} F - "when - sometime in the future will be true that ...“

} G - "always in the future will be true that ..." n P - "when - in the past it was true that ..."

13. What is Tense Logic, Formalized statements, LTL, Kripke structure - interpretation of formulas LTL,CTL and CTL*

X (Next time) Chronicle is true at time t, p is true if the next time (assuming discrete time points, the time t + 1)

Formalize statement:

} If the message m will arrive at the entrance to the channel, then sometime in the future, this message will appear at the output:

} input(m) => output (m)

} But this formalization is inadequate! The second statement is true at the same time, when the truth is the first! Meaning of the statement that we want to formalize:

} If the input at an arbitrary time t appeared message m, then at some point in time following t1, such that t <t1, the same message appears at the output

Correct statement

} "If the message m will arrive at the entrance to the channel, then sometime in the future it will output“

Kripke's structure is a final machine gun with not marked transitions with which each state some set of atomic statements, true in this state is connected

On a concrete chain of states (worlds) in each state we can calculate truthconditional values of any formula of temporal logic of LTL

In logic of CTL * the quantifiers of a way allowing to distinguish properties of various ways

CTL * are added is defined for concrete interpretation (Kripke's structure) and all its possible calculations of

CTL is CTL subset * - in formulas CTL each temporal operator is preceded by a quantifier of a way

Date: 2016-01-03; view: 1663