### PPT

```VERIFICATION OF
PARAMETERIZED SYSTEMS
MONOTONIC ABSTRACTION IN
PARAMETERIZED SYSTEMS
Parosh Aziz Abdullah, Giorgio Delzanno, Ahmed Rezine
NAVNEETA NAVEEN PATHAK
AGENDA

INTRODUCTION
 PARAMETERIZED
 TRANSITION
SYSTEMS
SYSTEMS
 ORDERING
 MONOTONIC ABSTRACTION
Monotonic Abstraction in Parameterized Systems
2
INTRODUCTION
Monotonic Abstraction as a simple and effective
method to prove safety properties for
Parameterized Systems with linear topologies.
Main idea : Monotonic Abstraction for
considering a transition relation that is an overapproximation of the one induced by the
parameterized system.
Monotonic Abstraction in Parameterized Systems
3
MODEL CHECKING + ABSTRACTION
Infinite-State
System
Abstraction
Model
Checking
Finite-State
System
Monotonic Abstraction in Parameterized Systems
4
AGENDA

INTRODUCTION
 PARAMETERIZED
 TRANSITION
SYSTEMS
SYSTEMS
 ORDERING
 MONOTONIC ABSTRACTION
Monotonic Abstraction in Parameterized Systems
5
PARAMETERIZED SYSTEMS
P1
P2
P3
PN
P4
P3
PN
.........
P2
P1
..........
.........
AIM : To verify correctness of the systems for the
whole family of Parameterized Systems.
Monotonic Abstraction in Parameterized Systems
6
DEFINITION
A parameterized system P is a triple (Q,X, T ),
Q - set of local states,
X - set of local variables,
T - set of transition rules.
A transition rule t is of the form:
t: [ q | grd → stmt | q´ ]
where q, q´ ϵ Q
grd → stmt is a guarded command
grd ϵ B(X) U G(X U Q)
stmt : set of assignments
Monotonic Abstraction in Parameterized Systems
7
Parameterized System, P = (Q,T)
A process Q = {Green, Black, Blue, Red} and T = {t t t t t t }
1, 2, 3. 4, 5, 6
moves from where t t t – Local transition
Idle State
–
Initially
all
rules
2, 5, 6
Idle to Black
processes are in this
t1, t4 – Universal Rules
state when it
state
t3 – Existential Rule
wants to
access its
critical
section.
Once a process
moves from Black
to Blue state, it
“closes the door”
on all processes in
Idle state
∃L
t3
V LR
t1
t2
t6
t5
Critical State –
Eventually a process
will enter this state
t4
VL
Monotonic Abstraction in Parameterized Systems
8
AGENDA

INTRODUCTION
 PARAMETERIZED
 TRANSITION
SYSTEMS
SYSTEMS
 ORDERING
 MONOTONIC ABSTRACTION
Monotonic Abstraction in Parameterized Systems
9
TRANSITION SYSTEMS
A transition system T is a pair (C,⇒)
where,
C - (infinite) set of configurations ,
⇒ - binary relation on C,
⇒* - reflexive transitive closure of ⇒
A configuration c ϵ C is a sequence u1 , ...... , un of process
states.
i.e. corresponding to an instance of the system with n
processes.
Monotonic Abstraction in Parameterized Systems
10
The word below represents a configuration in
an instance of system with 5 processes.
Valid Transitions
t3
Invalid Transitions
t3
Monotonic Abstraction in Parameterized Systems
11
Initial Configuration
All configurations that have atleast 2 RED processes
AIM : Init
*
Monotonic Abstraction in Parameterized Systems
12
AGENDA

INTRODUCTION
 PARAMETERIZED
 TRANSITION
SYSTEMS
SYSTEMS
 ORDERING
 MONOTONIC ABSTRACTION
Monotonic Abstraction in Parameterized Systems
13
ORDERING
c1, c2 – configurations
c1 ≤ c2 - c1is a subword of c2
e.g.
≤
Upward Closed Configurations
Set U of configurations is upward closed, if
whenever c ϵ U and c ≤ c´ then c´ϵ U.
c – configuration,
ĉ – denotes upward closed set U:= {c´ | c ≤ c´}
ĉ contains all configurations larger than c w.r.t. ordering ≤.
i.e. c is the generator of U
Monotonic Abstraction in Parameterized Systems
14
Why Upward Closed Sets ?
1. All sets of Bad configurations (which are worked upon)
are upward closed.
2. Upward closed sets have an efficient symbolic
representation.
i.e. For an upward closed set U, there are
configurations c1, ..... , cn with U = ĉ1 U......U ĉn
Monotonic Abstraction in Parameterized Systems
15
Coverability Problem for Parameterized
Systems
To analyze safety properties.
PAR-COV
Instance
• Parameterized System, P = (Q,X,T)
•CF – upward-closed set of configurations
Question
*
Init
CF ?
Monotonic Abstraction in Parameterized Systems
16
Backward Reachability Analysis
For a set of configurations, C
Use Pre(C) := {c | ∃c´ϵ C; c → c´}
IDEA :
ii. Apply function Pre repeatedly generating sequence U0,
U1, U2,.... where
U0 := Bad, and Ui+1 := Ui + Pre(Ui) for all i ≥ 0
Observation :
set Ui characterizes set of configurations from which
set Bad is reachable within i steps
Monotonic Abstraction in Parameterized Systems
17
MONOTONICITY
Monotonicity implies that upward closedness is preserved
through the application of Pre.
Consider:
U – upward closed set,
c1 – member of Pre(U) and c2 ≥ c1
By Monotonicity, it can be proved that
c2 is also a member of Pre(U)
Monotonic Abstraction in Parameterized Systems
18
AGENDA

INTRODUCTION
 PARAMETERIZED
 TRANSITION
SYSTEMS
SYSTEMS
 ORDERING
 MONOTONIC ABSTRACTION
Monotonic Abstraction in Parameterized Systems
19
MONOTONIC ABSTRACTION
An abstraction that generates over-approximation of the
transition systems.
The abstract transition system is monotonic.
Hence, allowing one to work with upward closed sets.
c1
c1´
≥
A
c2
Monotonic Abstraction in Parameterized Systems
20
Local transitions are monotonic!
Consider the local transition,
t2
c1 =
= c3
Configuration c2 =
c2 =
t2
c4
This leads to c4 ≥ c2 and also maintains c3 ≤ c4.
Monotonic Abstraction in Parameterized Systems
21
Existential transitions are monotonic!
Consider the existential transition:
t3
c1 =
= c3
Configuration, c2 =
t3
c2 =
= c4
Monotonic Abstraction in Parameterized Systems
22
Non-monotonicity of Universal
transitions
Consider the following Universal transition:
c1 =
t4
= c3
t4 can be applied to c1 as all process in the left context of the
active process satisfy the condition of transition.
Now consider c2 =
c 1 ≤ c2
But t4 is not enabled from c2 since the left context of the
active process violates the conditions of transition.
Monotonic Abstraction in Parameterized Systems
23
Solution!
1. Work with Abstract transition relation →A.
2. →A is an monotonic abstraction (over-approximation) of
the concrete relation →.
3. When t is universal,
t
t
we have: c1 →
c
iff
c
´
→
c2 for some c1´ ≤ c1
A 2
1
t4
→
i.e.
A
Since
≤
Monotonic Abstraction in Parameterized Systems
t4
→
24
Solution.....
Since,
 c1 ≤ c2
 c1 →A c3 implies c2 →A c3
Hence, Abstract transition relation is Monotonic, w.r.t.
Universal Transitions.
The Abstract transition relation is and over-approximation of
the original transition relation
↓↓
If a safety property holds in the abstract model, then it will
also hold in the concrete model.
Monotonic Abstraction in Parameterized Systems
25
Coverability Problem for Approximate
Systems
APRX-PAR-COV
Instance
• Parameterized System, P = (Q,X,T)
•CF – upward-closed set of configurations
Question
*
Init
A CF ?
Monotonic Abstraction in Parameterized Systems
26
A
1
=(
U
1)
reflects the approximation of universal quantifiers
Since
⊆
A
A negative answer to APRX-PAR-COV implies a negative
Monotonic Abstraction in Parameterized Systems
27
CONCLUSION
Monotonic Abstraction in Parameterized Systems
28
 Introduction to our topic.
 Overview of Parameterized Systems using a simple
example.
 (Infinite) Transition Systems arising from parameterized
systems.
 Introduced Ordering on the set of configurations.
 Definiton and explanation of Monotomic Abstraction; based
on the parameterized systems example.
Monotonic Abstraction in Parameterized Systems
29