Scribd Logo
Upload

Welcome to Scribd!

  • 61 views

    Formal Methods in Software Engineering

    Uploaded by

    lets play
    Temporal logic is a formal method used to model and specify concurrent systems. It treats the temporal aspects of system execution needed to monitor infinite behavior over time. Temporal logic uses additional operators beyond propositional logic to represent time and the relationships between time steps. There are two main types - linear temporal logic which has a single successor state at each time, and branching temporal logic where time splits into alternative paths. Key operators include "Globally" to represent something happening at all times, "Eventually" for something occurring at some future time, and "Until" for one thing remaining true until another occurs.

    Copyright:

    © All Rights Reserved
    Download as PDF, TXT or read online from Scribd

    Formal Methods in Software Engineering

    Uploaded by

    lets play
    61 views21 pages
    Temporal logic is a formal method used to model and specify concurrent systems. It treats the temporal aspects of system execution needed to monitor infinite behavior over time. Temporal logic uses additional operators beyond propositional logic to represent time and the relationships between time steps. There are two main types - linear temporal logic which has a single successor state at each time, and branching temporal logic where time splits into alternative paths. Key operators include "Globally" to represent something happening at all times, "Eventually" for something occurring at some future time, and "Until" for one thing remaining true until another occurs.

    Original Title

    Lecture 7

    Copyright

    © © All Rights Reserved

    Available Formats

    PDF, TXT or read online from Scribd

    Did you find this document useful?

    Is this content inappropriate?

    Temporal logic is a formal method used to model and specify concurrent systems. It treats the temporal aspects of system execution needed to monitor infinite behavior over time. Temporal logic uses additional operators beyond propositional logic to represent time and the relationships between time steps. There are two main types - linear temporal logic which has a single successor state at each time, and branching temporal logic where time splits into alternative paths. Key operators include "Globally" to represent something happening at all times, "Eventually" for something occurring at some future time, and "Until" for one thing remaining true until another occurs.

    Copyright:

    © All Rights Reserved
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    61 views21 pages

    Formal Methods in Software Engineering

    Uploaded by

    lets play
    Temporal logic is a formal method used to model and specify concurrent systems. It treats the temporal aspects of system execution needed to monitor infinite behavior over time. Temporal logic uses additional operators beyond propositional logic to represent time and the relationships between time steps. There are two main types - linear temporal logic which has a single successor state at each time, and branching temporal logic where time splits into alternative paths. Key operators include "Globally" to represent something happening at all times, "Eventually" for something occurring at some future time, and "Until" for one thing remaining true until another occurs.

    Copyright:

    © All Rights Reserved
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    You are on page 1of 21

    Formal Methods in Software Engineering

    Lecture 07
    What is Temporal Logic?

     Objective: We describe temporal aspects of formal methods to model and


    specify concurrent systems and verify their correctness properties.

     In concurrent reactive systems, correctness not only validates the correct input
    and output of the computational system, but also objectively monitors the
    execution of the system.

     Temporal logic is explicitly developed to treat these aspects and to monitor


    infinite behavior of reactive systems.
    ,
    What is Temporal Logic?

     Temporal logics have played vital role in formal verification wherever needed to
    state the specification requirements for hardware and software systems.

     Time: It represents the set of rules for reasoning in terms of time and the time
    domain is expressed in terms of state.

     A present time corresponds to current state and next moment of time


    corresponds to the immediate next state.

     Alternatively, system behavior is observed in terms of discrete time points such


    as 0, 1, 2,….., n.
    What is Temporal Logic?

     Transition: Transition corresponds to the progressions from current time step


    to the next time step with specific action.

     Temporal logic is applicable due to its behavioral aspects of hardware and


    software in terms of time.

     Reasoning in the temporal logic is much easier with the translation into the
    predicate calculus because relationship among time is implicit manner.
    Temporal Logic Operators

     Temporal logic has introduced some additional operators that represent the
    time variable and reflect their relationships.

     In essence, temporal logic is an extension of propositional logic. It is also


    known as propositional temporal logic (PTL).

     With the set of temporal operators, these enable the definition of formulas with
    the accessibility relation.

     When defining temporal properties, some temporal operators are needed to


    model the system in terms of time.
    Temporal Logic Operators

     These operators include


    F ----- Future or eventually
    G ---- Globally
    X ------ Next
    U ------ Unitl

     The first three operators are unary whereas the last one is binary
    Computational Paths, System run

     Define in terms of states and transitions

     A sequence of states, starting with an initial state


     s0 s1 s2 … such that R(si, si+1) is true

     Also called “run”, or “(computation) path”

     Trace: sequence of observable parts of states – Sequence of state labels


    Core Properties of Temporal Logic

     Safety property means “something bad must not happen”. E.g.: system should not crash.

     Liveness property means “something good must happen”. E.g.: every packet sent must
    be received at its destination

     Guarantee of Service states that if one process sends a request, it must have to be
    responded by other process.

     Mutually exclusion occur when two processes execute concurrently at the same critical
    section. Then, it is prescribed as “bad thing”.
    Temporal Logic Operators
    Temporal Logic Operators

    Globally (Always) p: G p
     G p is true for a computation path if p holds at all states
    (points of time) along the path
    Temporal Logic Operators

    Eventually p: F p
     F p is true for a path if p holds at some state along that
    path
    Temporal Logic Operators

    Next p: X p
     X p is true along a path starting in state si (suffix of the
    main path) if p holds in the next state si+1
    Temporal Logic Operators

    Examples: What do they mean?

     GFp

     FGp

     G( p  F q )

     F( p  (X X q) )
    Temporal Logic Operators

    p Until q: p U q
     p U q is true along a path starting at s if
     q is true in some state reachable from s
     p is true in all states from s until q holds
    Temporal Logic Types

     There are two types of temporal logics, each having their own temporal
    operators.

     In linear time temporal logic, there is a single successor state at each


    moment of time

     Branching time temporal logic, time is split into different alternative


    paths.
    Temporal Logic Models

     Linear Time Temporal Logic

     Branching time temporal logic


    Linear Time Temporal Logic (LTL)

     Linear Temporal Logic has been proposed as a formal verification tool by Amir
    Pnueli.

     LTL models time as a sequence of states and the future state is seen as a path
    in LTL.

     Accordingly, there are different future paths from where any path is taken as an
    actual path.

     There are many LTL model checking tools available which use LTL as a
    property specification language
    LTL Syntax
    LTL Semantics
    LTL Semantics

     The semantics is defined by induction on the structure of ⱷ, is given as:


    Thanks

    You might also like