Bchi Automata in Formal Systems - CS60030 Lecture Overview

BchiAutomata FORMAL SYSTEMS (CS60030) Pallab Dasgupta Professor, Dept. of Computer Sc & Engg INDIAN INSTITUTE OF TECHNOLOGY KHARAGPUR

Lecture Overview Motivation: Peterson s Algorithm -Regular Languages Nondeterministic B chi Automata (NBA) NBA and -Regular Languages 1

Recap: Verifying regular safety properties A safety property P is regular if bp(P) is a regular language Thus, bad prefixes of P are recognizable by an NFA A A Checking TS | | = P for regular P reduces to A A checking a (simple) invariant on the product automaton TS A A i.e., performing a simple depth-first search on TS Time and space complexity in O O ( |TS| . |A A|) for more general properties we need automata accepting infinite words! 2

Petersons banking system Person Left behaves as follows: Person Right behaves as follows: while true { while true { . . . . . . . . . . . . b1, x = true, 2; b2, x = true, 1; rq : rq : wait until(x == 1 || b2) { wait until(x == 2 || b1) { wt : wt : . . . @accountL. . .} . . . @accountR. . .} cs : cs : b1 = false; b2 = false; . . . . . . . . . . . . } } 3

Is the banking system live? x = = 1 x = = 2 b1 = 0 b2 = 0 b1 = 1 b2 = 1 x = 1 x = 2 b2 = 1 b1 = 1 x = 2 b1 = 0 b1 = 1 x = 2 x = 1 b2 = 1 x = 1 b2 = 0 x = = 1 x = = 2 If someone wants to update the account, does he ever get the opportunity to do so? always (reqL eventually @accountL) always (reqR eventually @accountR) 4

Is the banking system live (revisited)? Live = when you want access to the account, you eventually get it Unlive = when you want access to the account, you NEVER get it o An unlive behaviour can be characterized as a (set of) infinite traces o or, equivalently, by a B chi-automaton Live: @account true true req @account Checking liveness: ??????(????? ) ??(????) = ? (explicit) complementation, intersection and emptiness of B chi automata! 5

Lecture Overview Motivation: Peterson s Algorithm -Regular Languages Nondeterministic B chi Automata (NBA) NBA and -Regular Languages 6

Regular expressions Let ? be an alphabet with ? ? Regular expressions over ? have syntax: ?::= ? | ? | ? ? + ? ?. ? | ? The semantics of regular expression ? is a language ? ? ? : ? ? = ? ? ? = ? ? ? = ? ? ?.? = ? ? .?(? ) ? ? = ? ? ? ? + ? = ? ? ?(? ) 7

Syntax of -regular expressions Regular expressions denote languages of finite words -Regular expressions denote languages of infinite words An -regular expression? over ? has the form: ?+ + ??.???for n>0 ? = ?1.?1 where ??, ?? are regular expressions over ? with ? ?(??) Some examples: (? + ?) . ??, , (? . ?)? , , ? . ??+ ?? 8

Semantics of -regular expressions For ? ? let ??= ?1?2?3 ? 0. ?? ?} ?+ + ??.??? Let -regular expression ? = ?1.?1 The semantics of ? is the language ??? ??: ? ... ?(??).?(??)? ??? = ? ?1.? ?1 G1 and G2 are equivalent, denoted ?1 ?2 , if ???1= ???2 8

-Regular languages ? is -regular if ? = ??? for some -regular expression ? Examples over ? = {?,?}: Language of all words with infinitely many As: (? . ?)? Language of all words with finitely many As: (? + ?) . ?? The empty language: ? -Regular languages are closed under , and complementation 10

-Regular safety properties Definition: LT property P over AP is -Regular if P is an -regular language over the alphabet 2AP Or, equivalently: LT property P over AP is -Regular if P is a language accepted by a nondeterministic B chi automaton over 2AP 11

Abstract examples of -regular properties Any invariant P is an - regular property as ? described P with invariant condition Any regular safety property P is an -regular property as ? = ?? ? . ???? is ?-regular. And the fact that ? ?-regular languages are closed under complement. Any liveness property P is an -regular property 12

Concrete -regular properties 13

Lecture Overview Motivation: Peterson s Algorithm -Regular Languages Nondeterministic B chi Automata (NBA) NBA and -Regular Languages 6

Nondeterministic Bchi automata NFA (and DFA) are incapable of accepting infinite words Automata on infinite words suited for accepting -regular languages We consider nondeterministic B chi automata (NBA) Accepting runs have to check the entire input word are infinite acceptance criteria for infinite runs are needed NBA are like NFA, but have a distinct acceptance criterion one of the accept states must be visited infinitely often 14

Bchi automata A nondeterministic B chi automaton (NBA) ? is a tuple (Q, , , Q0, F ) where: Q is a finite set of states with Q0 Q a set of initial states is an alphabet : Q 2Q is a transition function F Q is a set of accept (or: final) states 15

An example NBA 16

Language of an NBA NBA ? = (Q, ?, ?, ??, F) and word ? = A0 A1 A2. . . ?? A run for ? in ? is an infinite sequence q0 q1 q2 . . . such that: ??+???+? for all ? ? ?? ?? and ?? Run q0 q1 q2 is accepting if ?? ? for infinitely many i i. . ? ?? is accepted by ? if there exists an accepting run for ? The accepted language of ? : ??? = ? ?? ? ??? ?????? ?? ????????? ??? ??? ? ?? ?} NBA ? and ? are equivalent if ??? = ??? 17

Example runs and accepted words 18

Some NBA for -regular properties 19

NBA versus NFA a a a a a a a a -equivalence finite equivalence finite equivalence -equivalence ? ? = ? (? ), but ??? ??? = ??? ,but ? ? ? (? ) ??? 20

Lecture Overview Motivation: Peterson s Algorithm -Regular Languages Nondeterministic B chi Automata (NBA) NBA and -Regular Languages 6

NBA and -regular languages The class of languages accepted by NBA agrees with the class of -regular languages. (1) any -regular language is recognized by an NBA (2) for any NBA A, the language L (A) is -regular 21

For any -regular language there is an NBA How to construct an NBA for the -regular expression: ?+ + ??.??? ? ? = ?1.?1 where ??, ?? are regular expressions over ? with ? ? ?? Use operators on NBA mimicking operators on -regular expressions: for NBA ?1 and ?2 there is an NBA accepting ???1 ???2 for any regular language ? with ? ? there is an NBA accepting ?? for regular language ? and NBA ? there is an NBA accepting ?.??? We will discuss these three operators in detail 22

Union of NBAs For NBA ?? and ?? (both over the alphabet ?) there exists an NBA ? such that: ??? = ???? ???? and ? = ?( ??+ ??) 23

Definition of -operator for NFA Let ? = (Q, ?, ?, Q0, F) be an NFA with ? ?(?). Assume no initial state in A has incoming transitions and ?? ? = Otherwise introduce a new initial state ???? ? A A ? iff ?? Keep all transitions in ? A A ? for some ?? ?? Let ???? Construct an NBA ? = (?, ?, ? , ? ?, ? ) as follows If ? A A ? ? then add ? Keep all transitions in ? ? ?= ?? and ? = ?? A A?? for any ?? ?? 24

Example for -operator for NFA A A B A B q 0 q 1 q0 q1 qnew B B A A B q 0 q 1 qnew B B From an NFA accepting A B to an NBA accepting (A B) 25

Proof of ??? ?(?)? Let ? ??(? ) and q0 q1 q2 be an accepting run for ? in ? Hence, ?? ? = ?? for infinitely many indices i Let ??= ? < ??< ??< such that ??? ? and ?? ? for ? ?? Divide ? into infinitely many nonempty finite sub-words ?? ? : ? = ?? ?? ?? such that ??? ? (??? ?,??) for all ? > ? It follows ? ??? ?,?? ? ? ??? ?? and ??? ?? has no incoming transitions, thus ??? ? Thus: ?? ?(?) for any ? > 0, and hence ? ?(?)? 26

Proof of ????(?)? Let ? = ?? ?? ?? such that ?? ?(?) for all ? > 0 That is, ? ?(?)? ? ?? ? ?? ? ??? Let ?? ? be an accepting run for ?? in ? ?+? ? (?? ?,??)for all ? > ? By definition of ? , we have ?? ? ??? ? ? ? ??? ? ? ? ??? ? ? ?? is an accepting run for ? in ? ?? ?? Hence ? ??(?) 27

Summarizing: -operator for NFA For each NFA ? with ? ? ? there exists an NBA ? such that: ??? = ? ?? and A = O( ? ) 28

Concatenating an NFA and an NBA For NFA ? and NBA ? (both over the alphabet ) there exists an NBA ? with: ??? = ? ? .??? and A = O( ? + ? ) 29

Summarizing the results so far For any -regular language L there exists an NBA ? with ??? = ? 30