Analyzing Timed Systems Using Tree Automata

(1)

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

Analyzing Timed Systems Using Tree Automata

S Akshay¹, Paul Gastin² and Krishna Shankara Narayanan¹

1Dept of CSE, IIT Bombay, India,

2LSV, ENS Cachan, France.

CONCUR 2016, Quebec 26 Aug 2016

1

(2)

Timed automata and timed runs

q1 x≤3 q2

a,x := 0

(3)

Timed automata and timed runs

q1 x≤3 q2 q3

a,x:= 0

y ≥4 b,y:= 0

x≤2 a,x:= 0

X ⁰ ^a,³ ^b,⁴ ^a,⁵

2

(4)

Timed automata and timed runs

q1 x≤3 q2 q3

a,x:= 0

y ≥4 b,y:= 0

x≤2 a,x:= 0

X ⁰ ^a,³ ^b,⁴ ^a,⁵

× ⁰ ^a,³ ^b,⁵ ^a,⁷

× ⁰ â,³ ^b,⁴ â,⁵ â,⁸ â,⁷

(5)

Timed automata and timed runs

q1 x≤3 q2 q3

a,x:= 0

y ≥4 b,y:= 0

x≤2 a,x:= 0

X ⁰ ^a,³ ^b,⁴ ^a,⁵

× ⁰ ^a,³ ^b,⁵ ^a,⁷

× ⁰ â,³ ^b,⁴ â,⁵ â,⁸ â,⁷

The timed languageL_T(A) = set of suchgood timed words Emptiness problem : GivenA, is L_T(A) =∅?

2

(6)

Emptiness for timed automata

A well-studied problem with a now standard approach

many optimizations since... Timed pushdown automata:

Our point-de-depart

representbehaviors as graphs with timing constraints use tree interpretations to reduce to tree automata

(7)

Emptiness for timed automata

A well-studied problem with a now standard approach Timed automata: Region construction [Alur-Dill’90], and many optimizations since...

Timed pushdown automata:

Our point-de-depart

3

(8)

Emptiness for timed (pushdown) automata

Timed pushdown automata:

(9)

Emptiness for timed (pushdown) automata

Timed pushdown automata: Lifting region construction – [Bouajjani et al. ’94],[Abdulla et al. 2012]

Our point-de-depart

3

(10)

Emptiness for timed (pushdown) automata

An orthogonal approach: [Clemente-Lasota 2015]

(11)

Emptiness for timed (pushdown) automata

Common feature:

represent behaviors as timed words and,

use abstractions to reduce to finite automata over words

Our point-de-depart

3

(12)

Emptiness for timed (pushdown) automata

Common feature:

Our point-de-depart

(13)

Emptiness for timed (pushdown) automata

Common feature:

Our point-de-depart

A higher level and more powerful formalism Yields simpler proofs for more complicated systems A new technique which does not depend on regions/zones

3

(14)

Outline

1 Timed behaviours as graphs

2 Checking realizability

3 Interpreting graphs into trees

4 Bounding the (split-)width of graphs

5 Conclusion & future work

(15)

Abstracting paths of a timed system as graphs

q1 x≤3 q2 q3

a,x:= 0

y≥4 b,y:= 0

x≤2 a,x:= 0

a b a

≤3 ≤2

≥4

5

(16)

Abstracting paths of a timed system as graphs

q1 x≤3 q2 q3

a,x:= 0

y≥4 b,y:= 0

x≤2 a,x:= 0

a b a

≤3 ≤2

≥4

a b a b a

≤3 ≤2

≥4

≤2

≥4

(17)

Abstracting paths of a timed system as graphs

q1 x≤3 q2 q3

a,x:= 0

y≥4 b,y:= 0

x≤2 a,x:= 0

a b a

≥0 ≥0 ≥0

≤3 ≤2

≥4

a b a b a

≥0 ≥0 ≥0 ≥0 ≥0

≤3 ≤2

≥4

≤2

≥4

5

(18)

Abstracting paths of a timed system as graphs

q1 x≤3 q2 q3

a,x:= 0

y≥4 b,y:= 0

x≤2 a,x:= 0

a b a

≥0 ≥0 ≥0

≤3 ≤2

≥4

a b a b a

≥0 ≥0 ≥0 ≥0 ≥0

≤3 ≤2

≥4

≤2

≥4

set of such time-constrained graphs, TC-words = L_TCW(A).

(19)

Abstracting paths of a timed system as graphs

q1 x≤3 q2 q3

a,x:= 0

y≥4 b,y:= 0

x≤2 a,x:= 0

a b a

≥0 ≥0 ≥0

≤3 ≤2

≥4

a b a b a

≥0 ≥0 ≥0 ≥0 ≥0

≤3 ≤2

≥4

≤2

≥4

set of such time-constrained graphs, TC-words =L_TCW(A).

What are some properties of such graphs?

5

(20)

Abstracting paths of a timed system as graphs

q1 x≤3 q2 q3

a,x:= 0

y≥4 b,y:= 0

x≤2 a,x:= 0

a b a

≥0 ≥0 ≥0

≤3 ≤2

≥4

a b a b a

≥0 ≥0 ≥0 ≥0 ≥0

≤3 ≤2

≥4

≤2

≥4

set of such time-constrained graphs, TC-words =L_TCW(A).

What are some properties of such graphs?

What is the link betweenLTCW(A) andLT(A)?

(21)

TC-words and their relation to timed words

Properties of TC-words and timed words

1 Not all (linearly-ordered) graphs are TC-words

a b a

6

(22)

TC-words and their relation to timed words

X ^a ^b ^a

(23)

TC-words and their relation to timed words

× ^a ^b ^a

This graph cannot be generated by any timed automaton.

6

(24)

TC-words and their relation to timed words

× â â â ^b ^b

(25)

TC-words and their relation to timed words

X â â â ^b ^b

But, it can be generated by a timed pushdown automaton!.

6

(26)

TC-words and their relation to timed words

2 A TC-word can berealized by (infinitely) many timed words

X ^≥⁰ ^a ^≥⁰ ^b ^≥⁰ ^a

≤3 ≤2

≥4

ǫ,0 a,3 b,4 a,5

ǫ,0 a,2.4 b,4.3 a,4.3

(27)

TC-words and their relation to timed words

2 A TC-word can berealized by (infinitely) many timed words

3 However, a TC-word may berealized by no timed word too!

a b a

≥0 ≥0 ≥0

≤3 ≤2

≥4

a b a b a

≤3 ≤2

≥4

≤2

≥4

≥0 ≥0 ≥0 ≥0 ≥0

6

(28)

Realizability of TC-words

Realizationof a TC-word is a timed word satisfying constraints A TC-word isrealizable if it has a timed word realization.

(29)

Realizability of TC-words

Recall: for a timed system A,L_TCW(A) denotes the set of TC-words accepted by it.

7

(30)

Realizability of TC-words

Difference betweenL_TCW(A) andL_T(A):

q1 x≤3 q2 q3

a,x:= 0

y≥4 b,y:= 0

x≤2 a,x:= 0

ǫ,0 a,2.5 b,4.2 a,4.4

a b a

≥0 ≥0 ≥0

≤3 ≤2

≥4

L_TCW(A) is over a finite alphabet, while L_T(A) is not.

(31)

Realizability of TC-words

Theorem: L_T(A) = Realizations(L_TCW(A))

7

(32)

Realizability of TC-words

The Emptiness problem

For a given timed (pushdown) automatonA,

L_T(A)6=∅ iff there exists a realizable TC-word inL_TCW(A).

(33)

Realizability of TC-words

The Emptiness problem

L_T(A)6=∅ iff there exists a realizable TC-word inL_TCW(A).

Thus, the question is: how to reason about these graphs?

7

(34)

Checking realizability of a single TC-word

a b a b a

≤3 ≤2

≥4

≤2

≥4

≥0 ≥0 ≥0 ≥0 ≥0

(35)

Checking realizability of a single TC-word

a b a b a

≤3 ≤2

≥4

≤2

≥4

≥0 ≥0 ≥0 ≥0 ≥0

a b a b a

0 0 0 0 0

3 2

−4

2

−4

8

(36)

Checking realizability of a single TC-word

a b a b a

≤3 ≤2

≥4

≤2

≥4

≥0 ≥0 ≥0 ≥0 ≥0

a b a b a

0 0 0 0 0

3 2

−4

2

−4

A simple exercise

A TC-word is realizable iff its directed graph has no negative cycle.

(37)

The Emptiness problem

Does there exist a TC-word inL_TCW(A), whose directed graph has no negative cycle?

How to reason about the set of graphs L_TCW(A)?

9

(38)

The Emptiness problem

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

(39)

The Emptiness problem

Graphs are well-formed

Graphs define an abstract path in the given timed system.

Graphs are realizable, i.e., no negative weight cycle.

9

(40)

The Emptiness problem

Then, by Courcelle’s theory, we obtain a finite tree automaton (by interpreting the graphs into trees).

(41)

The Emptiness problem

Same strategy as [Madhusudan & Parlato’11, Aiswarya et al

’12]for untimed pushdown systems.

9

(42)

The Emptiness problem

We show

Step 1: graphs from T(PD)A have a bounded (split-)width.

(43)

The Emptiness problem

Graphs from timed systems are different!

We show

9

(44)

The Emptiness problem

We show

(45)

The Emptiness problem

X Graphs are well-formed

X Graphs define an abstract path in the given timed system.

? Graphs are realizable, i.e., no negative weight cycle.

We show

9

(46)

The Emptiness problem

X Graphs are well-formed

X Graphs define an abstract path in the given timed system.

? Graphs are realizable, i.e., no negative weight cycle.

We show

Step 2: directly build a finite bottom-up tree automaton.

(47)

Complexity bounds

Step 1: Bound on (split-)width for timed (pushdown) systems Step 2: Directly building the tree automaton allows us to get tight complexity bounds.

10

(48)

Complexity bounds

Main results

1 For timed automaton Awith clocks X, all simple TC-words of Ahave (split-)width K ≤ |X|+ 4 .

(49)

Complexity bounds

Main results

1 For timed (pushdown) automatonAwith clocks X, all simple TC-words of A have (split-)widthK ≤ |X|+ 4(4|X|+ 6).

10

(50)

Complexity bounds

Main results

2 We can build a tree automaton of size exponential inK² to check realizability (details in paper).

(51)

Complexity bounds

Main results

3 Corollary: PSPACE (Exptime) emptiness for timed (pushdown) automata.

10

(52)

Complexity bounds

Main results

3 Corollary: PSPACE (Exptime) emptiness for timed (pushdown) automata.

Lift to timed multi-pushdown systems with bounded rounds Easy generalization, new decidability result & complexity too!

(53)

Step 0: Simplifying the TC-words

We first break TC-words into “simpler” graphs, so that each node has only one upper/lower time constraint attached to it.

For example,

is converted to:

To maintain atomicity, we use a single extra clock & add a constraint to each event:

ai [0,0]

11

(54)

Step 0: Simplifying the TC-words

For example,

ai [0,0]

(55)

Step 0: Simplifying the TC-words

For example,

is converted to:

ai [0,0]

11

(56)

Step 0: Simplifying the TC-words

For example,

is converted to:

ai [0,0]

(57)

Step 1: Split-width for timed systems

Now, define split game (see[Aiswarya et. al.’12, ’15])...

12

(58)

Step 1: Split-width for timed systems

Eve tries to disconnect the graph by cutting process edges.

Positions are simple TC-words with holes.

(59)

Step 1: Split-width for timed systems

Eve tries to disconnect the graph by cutting process edges.

Positions are simple TC-words with holes.

Adam chooses which connected component to continue.

12

(60)

Step 1: Split-width for timed systems

Game ends at atomic nodes (no process edges left).

(61)

Step 1: Split-width for timed systems

Width of such a split simple TC-word = no. ofblocksin it.

Cost of play = max width of split TC-word seen along play.

Split-width = min cost that Eve can achieve.

12

(62)

Step 1: Split-width for timed systems

To bound: split-width of any well-formed simple TC-word, i.e., graph from a timed (pushdown) automaton.

(63)

Step 1: Split-width for timed systems

13

(64)

Step 1: Split-width for timed systems

Let’s play the game...

(65)

Split-width for timed automata

14

(66)

Split-width for timed automata

(67)

Split-width for timed automata

14

(68)

Split-width for timed automata

(69)

Split-width for timed automata

For any TC-word of a timed automaton In any move of the game, we have:

Each hole is attached to last reset of a clock, holes only widen!

14

(70)

Split-width for timed automata

For any TC-word of a timed automaton In any move of the game, we have:

Each hole is attached to last reset of a clock, holes only widen!

Thus, no. of blocks ≤No. of clocks + 4.

(71)

Split-width for timed pushdown automata

15

(72)

Split-width for timed pushdown automata

(73)

Split-width for timed pushdown automata

15

(74)

Split-width for timed pushdown automata

(75)

Split-width for timed pushdown automata

For any TC-word of a timed pushdown automaton In any move of the game, we have:

Number of blocks ≤4·No. of clocks + 6.

15

(76)

Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

2 Show a bound on widthof graphs in L_TCW(A).

3 Interpret graphs into trees andreduce to a tree automaton B s.t., Realizations(L_TCW(A)) =∅ iff L(B) =∅.

A common framework for timed, pushdown, multi-pushdown automata with bounded rounds.

Robust framework: diagonal guards, etc. Future work

Concurrent recursive timed programs MSO definability of realizability

Going beyond emptiness. What about model-checking?

(77)

Conclusion and Future work

1 Writebehaviors as graphs with timing constraints L_TCW(A).

2 Show a bound on widthof graphs in L_TCW(A).

16

(78)

Conclusion and Future work

2 Show abound on width of graphs in L_TCW(A).

s.t., Realizations(L_TCW(A)) =∅ iff L(B) =∅.

(79)

Conclusion and Future work

3 Interpret graphs into trees andreduce to a tree automaton B

s.t., Realizations(L_TCW(A)) =∅ iff L(B) =∅.

16

(80)

Conclusion and Future work

automata with bounded rounds.

(81)

Conclusion and Future work

16

(82)

Conclusion and Future work

Robust framework: diagonal guards, etc.

(83)

Conclusion and Future work

Robust framework: diagonal guards, etc.

Future work

16