Name
Abstract | ||
|---|---|---|
In this paper we describe an extension of timed automata with priorities, and efficient algorithms to compute subtraction on DBMs (difference bounded matrices), needed in symbolic model-checking of timed automata with priorities. The subtraction is one of the few operations on DBMs that result in a non-convex set needing sets of DBMs for representation. Our subtraction algorithms are efficient in the sense that the number of generated DBMs is significantly reduced compared to a naive algorithm. The overhead in time is compensated by the gain from reducing the number of resulting DBMs since this number affects the performance of symbolic model-checking. The uses of the DBM subtraction operation extend beyond timed automata with priorities. It is also useful for allowing guards on transitions with urgent actions, deadlock checking, and timed games. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11867340_10 | FORMATS |
Keywords | Field | DocType |
naive algorithm,urgent action,deadlock checking,model checking,subtraction algorithm,symbolic model-checking,difference bounded matrix,efficient algorithm,dbm subtraction operation,subtraction,convex set,dbm | Model checking,Computer science,Deadlock,Automaton,Binary decision diagram,Theoretical computer science,Timed automaton,Formal methods,Subtraction,Mutual exclusion,Distributed computing | Conference |
Volume | ISSN | ISBN |
4202 | 0302-9743 | 3-540-45026-2 |
Citations | PageRank | References |
20 | 1.34 | 22 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexandre David | 1 | 1667 | 76.52 |
| John Håkansson | 2 | 229 | 13.36 |
| Kim G. Larsen | 3 | 3922 | 254.03 |
| Paul Pettersson | 4 | 2636 | 174.89 |