Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Analyzing Timed Systems Using Tree Automata

S Akshay^{1}, Paul Gastin^{2} and Krishna Shankara Narayanan^{1}

1Dept of CSE, IIT Bombay, India,

2LSV, ENS Cachan, France.

CONCUR 2016, Quebec 26 Aug 2016

1

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Timed automata and timed runs

q1 x≤3 q2

a,x := 0

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Timed automata and timed runs

q1 x≤3 q2 q3

a,x:= 0

y ≥4 b,y:= 0

x≤2 a,x:= 0

X ^{0} ^{a,}^{3} ^{b,}^{4} ^{a,}^{5}

2

## Timed automata and timed runs

q1 x≤3 q2 q3

a,x:= 0

y ≥4 b,y:= 0

x≤2 a,x:= 0

X ^{0} ^{a,}^{3} ^{b,}^{4} ^{a,}^{5}

× ^{0} ^{a,}^{3} ^{b,}^{5} ^{a,}^{7}

× ^{0} ^{a,}^{3} ^{b,}^{4} ^{a,}^{5} ^{a,}^{8} ^{a,}^{7}

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Timed automata and timed runs

q1 x≤3 q2 q3

a,x:= 0

y ≥4 b,y:= 0

x≤2 a,x:= 0

X ^{0} ^{a,}^{3} ^{b,}^{4} ^{a,}^{5}

× ^{0} ^{a,}^{3} ^{b,}^{5} ^{a,}^{7}

× ^{0} ^{a,}^{3} ^{b,}^{4} ^{a,}^{5} ^{a,}^{8} ^{a,}^{7}

The timed languageL_{T}(A) = set of suchgood timed words
Emptiness problem : GivenA, is L_{T}(A) =∅?

2

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

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

3

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Emptiness for timed (pushdown) automata

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

Timed pushdown automata:

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Emptiness for timed (pushdown) automata

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

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

Our point-de-depart

3

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Emptiness for timed (pushdown) automata

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

An orthogonal approach: [Clemente-Lasota 2015]

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Emptiness for timed (pushdown) automata

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

Common feature:

represent behaviors as timed words and,

use abstractions to reduce to finite automata over words

Our point-de-depart

3

## Emptiness for timed (pushdown) automata

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

Common feature:

represent behaviors as timed words and,

use abstractions to reduce to finite automata over words

Our point-de-depart

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Emptiness for timed (pushdown) automata

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

Common feature:

represent behaviors as timed words and,

use abstractions to reduce to finite automata over words

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

## 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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

## 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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

## 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).

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

## 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)?

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

## TC-words and their relation to timed words

Properties of TC-words and timed words

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

X ^{a} ^{b} ^{a}

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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}

This graph cannot be generated by any timed automaton.

6

## 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} ^{a} ^{a} ^{b} ^{b}

This graph cannot be generated by any timed automaton.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## TC-words and their relation to timed words

Properties of TC-words and timed words

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

X ^{a} ^{a} ^{a} ^{b} ^{b}

This graph cannot be generated by any timed automaton.

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

6

## TC-words and their relation to timed words

Properties of TC-words and timed words

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

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

X ^{≥}^{0} ^{a} ^{≥}^{0} ^{b} ^{≥}^{0} ^{a}

≤3 ≤2

≥4

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

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## TC-words and their relation to timed words

Properties of TC-words and timed words

1 Not all (linearly-ordered) graphs are TC-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

## 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.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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.

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

7

## 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.

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

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.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Realizability of TC-words

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

Theorem: L_{T}(A) = Realizations(L_{TCW}(A))

7

## Realizability of TC-words

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

Theorem: L_{T}(A) = Realizations(L_{TCW}(A))

The Emptiness problem

For a given timed (pushdown) automatonA,

L_{T}(A)6=∅ iff there exists a realizable TC-word inL_{TCW}(A).

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Realizability of TC-words

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

Theorem: L_{T}(A) = Realizations(L_{TCW}(A))

The Emptiness problem

For a given timed (pushdown) automatonA,

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

## Checking realizability of a single TC-word

a b a b a

≤3 ≤2

≥4

≤2

≥4

≥0 ≥0 ≥0 ≥0 ≥0

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

## 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.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## The Emptiness problem

For a given timed (pushdown) automatonA,

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

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

Graphs are well-formed

Graphs define an abstract path in the given timed system.

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

9

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

Graphs are well-formed

Graphs define an abstract path in the given timed system.

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

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

Graphs are well-formed

Graphs define an abstract path in the given timed system.

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

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

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

’12]for untimed pushdown systems.

9

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

Graphs are well-formed

Graphs define an abstract path in the given timed system.

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

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

We show

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

Graphs from timed systems are different!

We show

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

9

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

Graphs are well-formed

Graphs define an abstract path in the given timed system.

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

We show

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

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 1: graphs from T(PD)A have a bounded (split-)width.

9

## The Emptiness problem

For a given timed (pushdown) automatonA,

Does there exist a TC-word inL_{TCW}(A), whose directed graph
has no negative cycle?

If we can show that:

1 Graphs have a bounded-width.

2 Each property is expressible in MSO.

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 1: graphs from T(PD)A have a bounded (split-)width.

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

## 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.

Main results

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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.

Main results

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

10

## 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).

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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).

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

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

10

## Complexity bounds

Main results

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

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!

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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:

*a**i*
[0,0]

11

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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,

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

*a**i*
[0,0]

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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:

*a**i*
[0,0]

11

## Step 0: Simplifying the TC-words

For example,

is converted to:

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

*a**i*
[0,0]

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Step 1: Split-width for timed systems

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

12

## Step 1: Split-width for timed systems

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

Eve tries to disconnect the graph by cutting process edges.

Positions are simple TC-words with holes.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Step 1: Split-width for timed systems

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

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

## Step 1: Split-width for timed systems

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

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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Step 1: Split-width for timed systems

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

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

## 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.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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.

13

## 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.

Let’s play the game...

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Split-width for timed automata

14

## Split-width for timed automata

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Split-width for timed automata

14

## Split-width for timed automata

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

## 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.

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Split-width for timed pushdown automata

15

## Split-width for timed pushdown automata

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Split-width for timed pushdown automata

15

## Split-width for timed pushdown automata

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## 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?

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

1 Writebehaviors as graphs with timing constraints L_{TCW}(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?

16

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

1 Writebehaviors as graphs with timing constraints L_{TCW}(A).

2 Show abound on width of graphs in L_{TCW}(A).

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?

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

1 Writebehaviors as graphs with timing constraints L_{TCW}(A).

2 Show abound on width of 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?

16

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

1 Writebehaviors as graphs with timing constraints L_{TCW}(A).

2 Show abound on width of 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) =∅.

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?

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

1 Writebehaviors as graphs with timing constraints L_{TCW}(A).

2 Show abound on width of graphs in L_{TCW}(A).

_{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?

16

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

1 Writebehaviors as graphs with timing constraints L_{TCW}(A).

2 Show abound on width of graphs in L_{TCW}(A).

_{TCW}(A)) =∅ iff L(B) =∅.

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

Robust framework: diagonal guards, etc.

Concurrent recursive timed programs MSO definability of realizability

Going beyond emptiness. What about model-checking?

Introduction Graph behaviors Realizability Emptiness Split-width Conclusion

## Conclusion and Future work

A new recipe for analyzing timed systems. Given A,

1 Writebehaviors as graphs with timing constraints L_{TCW}(A).

2 Show abound on width of graphs in L_{TCW}(A).

_{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?

16