{"id":216,"date":"2017-12-22T03:18:00","date_gmt":"2017-12-22T03:18:00","guid":{"rendered":"https:\/\/kindsonthegenius.com\/blog\/2017\/12\/22\/basic-formalisms-for-design-modelling\/"},"modified":"2017-12-22T03:18:00","modified_gmt":"2017-12-22T03:18:00","slug":"basic-formalisms-for-design-modelling","status":"publish","type":"post","link":"https:\/\/kindsonthegenius.com\/blog\/basic-formalisms-for-design-modelling\/","title":{"rendered":"Basic Formalisms for Design Modelling"},"content":{"rendered":"
\n
In this article we would discuss five basic formalism for design modelling. They are:<\/p>\n
    \n
  1. Kripke Structure<\/li>\n
  2. Kripke Transition System<\/li>\n
  3. Labelled Transition System<\/li>\n
  4. Finite State Automata <\/li>\n
  5. Timed Automata<\/li>\n<\/ol>\n

    2. Kripke Structure<\/b>
    Kripke Structure is a kind of transition system used in Model Checking to represent the behavior of a system. It is represented as a directed graph where the nodes represent the reachable states of the system and the edges represents the state transitions.
    A function is used to map each of the nodes to a set of properties that hold true in that particular state<\/p>\n

    Formal Definition of Kripke Structure<\/b>
    Assuming AP is a set of atomic propostions (a boolean expressions over set of symbols, variable and constants), Kripke structure is defined over AP as a tuple T = {S, I, R, L} consisting of<\/p>\n

    S = {s1, s2, s2,…, sn} representing a finite set of states
    I = set of initial states (subset of S)
    R = set of transitions
    L = labeling of the state such that L<\/i>: <\/span>S<\/i> \u2192 2<\/span>AP<\/i><\/sup> <\/span><\/p>\n

    Example of Kripke Structure<\/b>
    An example of the Kripke Structure is the process model shown in the Figure 1.<\/p>\n\n\n\n\n
    <\/a><\/td>\n<\/tr>\n
    Figure 1: Kripke Structure for the Process Model<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

    Figure 1 illustrates Kripke structure for T = {S, I, R, L} where
    S = { s1, s2, s3, s4, s5}
    I = {s1}
    R = {(s1, s2), ( s2, s3), (s3,s4), (s4,s5), (s3,s2), (s3,s5), (s5,s2)}
    AP = {New, Ready, Running, Exit, Blocked}
    We can also write L by mapping the transition states to the atomic propositions.<\/p>\n

    Notes on Kripke Structure<\/b>
    Could have more than one label per transition
    Expresses properties of state and transition
    Could be  used to model algorithms<\/p>\n

     3. Labelled Transition System<\/b>
    A labelled transition system is made up of a set of states and a set of transitions between those states. These transitions are labelled by actions. One of the states is the initial state.<\/p>\n

    Formal Definition of Labelled Transition System<\/b>
    A labelled transition system (LTS) over a set of actions is given by:
    S = finite set of states
    A = Set of actions<\/p>\n\u2192\u2286<\/mo> S<\/mi> \u00d7<\/mo> A<\/mi> \u00d7<\/mo> S is a set of transitions<\/mi><\/math>\n

    <\/p>\ns0 is the initial state<\/mi><\/math>\n

    <\/p>\nNote on Labelled Transition System<\/mi><\/math>\n

    <\/b><\/p>\n

      \n
    • \nHas on action per transition<\/mi><\/math>\n<\/li>\n
    • \nExpresses properties of transitions<\/mi><\/math>\n<\/li>\n
    • \nCould be applied in modelling communication protocols <\/mi><\/math>\n<\/li>\n<\/ul>\nIn the next part we would continue with<\/mi><\/math>\n<\/div>\n
        \n
      • \nKripke Transition System<\/mi><\/math>\n<\/li>\n
      • \nFinite State Automata<\/mi><\/math>\n<\/li>\n
      • \nTimed Automata <\/mi><\/math>\n<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

        In this article we would discuss five basic formalism for design modelling. They are: Kripke Structure Kripke Transition System Labelled Transition System Finite State Automata … <\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_mi_skip_tracking":false,"_monsterinsights_sitenote_active":false,"_monsterinsights_sitenote_note":"","_monsterinsights_sitenote_category":0},"categories":[359],"tags":[],"_links":{"self":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/216"}],"collection":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/comments?post=216"}],"version-history":[{"count":0,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/216\/revisions"}],"wp:attachment":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/media?parent=216"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/categories?post=216"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/tags?post=216"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}