Model Checking in Formal Systems Overview
Explore the overview of LTL Model Checking in Formal Systems taught by Professor Pallab Dasgupta at the Indian Institute of Technology, Kharagpur, covering topics like negation of property, system persistence, transition systems, GNBA construction, and elementary sets.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
LTL Model Checking FORMAL SYSTEMS (CS60030) Pallab Dasgupta Professor, Dept. of Computer Sc & Engg INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
LTL Model Checking An Overview Negation of property System A persistence property for an NBA ? is FG ( no final state ) LTL formula ? Model of system Generalised B chi Automaton ? ? B chi automaton ? ? Transition system TS Product transition system ?? ? ? Check Model Checker ?? ? ? ?????(?) Yes No (counter-example) 2 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
Taking the Product : ?? ?? For a transitions system TS = (S, Act, , I, AP, L), without terminal states, and a non-blocking NBA ?=(Q, ?, ?, Q0, F) where ? = ??? , let: TS ? = (S , Act, , I , AP , L ) where, S = S X Q, AP = Q, and L (<s,q>) = {q} ? t t q q < <s s , , q> q> ?(?)? is the smallest relation defined by : s s ? < <t t , ?> ?(??) ? } I = {< <s s0 0 , , q> q> | s0 I ?? ?? .?? q is a state that is reached via a transition from some q0 ??labeled with L(s0) 3 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
From LTL to GNBAs For LTL property ? (for a transition system over AP), construct GNBA ?? over ??? with ???? = ?????(?). Assume ? contains operators , ,O,U. States of the GNBA: Elementary sets of sub-formulas in ? ? Transitions between states of the GNBA: derived from the O and U operator expansion laws. Accept states guarantee that: ? is an accepting run in ?? iff ? ? ? over states of the GNBA (elementary sets) over ??? for TS 4 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
Elementary Sets (the states of the GNBA) for ? ? For ? = A0 A1 A2 ?????(? ?) ), , each Ai ??. For each Ai we construct Bi (a set of sub-formula of ? ?), to obtain word ? = B0 B1 B2 such that: ? ?? if and only if ?? = Ai Ai+1 Ai+2 ? What should the initial state of the GNBA contain in its elementary sets? ? should be a run of the GNBA ?? for a word ?. 5 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
Elementary Sets for ? ? : Computing Closure of ? ? Closure. For an LTL-property ? ?, the set closure(? ?) consists of: All sub-formulas ? of ? ? and their negation ?. EXAMPLE: a U ( a b) Can we take Bi to be any subset of the closure(? ?)? NO! They must be elementary consistent (logically and locally) & maximal. 6 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
Elementary Sets for ? ? The set B closure(? ?) is elementary if: 1. B is logically consistent - if for all ? ?1 ? ?2 , ? closure(? ?): ? ?1 ? ?2 ? ? ?1 ? and ? ?2 ? ? ? ? ? true closure(? ?) true ? 2. B is locally consistent if for all ? ?1 U ? ?2 closure(? ?): ? ?2 ? ? ?1 U ? ?2 ? ? ?1 U ? ?2 ? and ? ?2 ? ? ?1 ? 3. B is maximal for all ? closure(? ?): ? ? ? ? 7 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
Examples: 8 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
The GNBA for the LTL-property ? ? For the LTL-property ? ?, let ?? = (Q, 2AP, ?, Q0, ?), where Q is the set of elementary sets of formulas B closure(? ?). Q0 = { B Q | ? ? ?} ? = { { B Q | ? ?1 U ? ?2 ? or ? ?2 ?} | ? ?1 U ? ?2 closure(? ?) } The transition relation ?: Q x 2AP Q is given by: ?( B, B ?? ) is the set of all elementary sets of formulas B satisfying: For every O? closure(? ?) : O? ? ? ? AND For every ? ?1 U ? ?2 closure(? ?): ? ?1 U ? ?2 ? (? ?2 ? ? ?1 ? ? ?1 U ? ?2 ? ) 9 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
GNBA for ? ? = Oa 10 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
GNBA for ? ? = a U b 11 INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR
