Lower and upper bounds in zone based abstractions of timed automata

Gerd Behrmann; Patricia Bouyer; Kim G. Larsen; Radek Pelánek

doi:10.1007/b96393

Lower and upper bounds in zone based abstractions of timed automata

Gerd Behrmann
, Patricia Bouyer
, Kim G. Larsen
, Radek Pelánek

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

38 Citations (Scopus)

145 Downloads (Pure)

Abstract

Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker UPPAAL.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings
Editors	Kurt Jensen, Andreas Podelski
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	312-326
ISBN (Electronic)	978-3-540-24730-2
ISBN (Print)	978-3-540-21299-7
DOIs	https://doi.org/10.1007/b96393
Publication status	Published - 29 Mar 2004
Event	10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004 - Barcelona, Spain Duration: 29 Mar 2004 → 2 Apr 2004 Conference number: 10

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2988
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004
Abbreviated title	TACAS
Country/Territory	Spain
City	Barcelona
Period	29/03/04 → 2/04/04

Keywords

n/a OA procedure

Access to Document

10.1007/b96393

ArticleAccepted author version, 625 KB

Cite this

Behrmann, G., Bouyer, P., Larsen, K. G., & Pelánek, R. (2004). Lower and upper bounds in zone based abstractions of timed automata. In K. Jensen, & A. Podelski (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings (pp. 312-326). (Lecture Notes in Computer Science; Vol. 2988). Springer. https://doi.org/10.1007/b96393

Behrmann, Gerd ; Bouyer, Patricia ; Larsen, Kim G. et al. / Lower and upper bounds in zone based abstractions of timed automata. Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. editor / Kurt Jensen ; Andreas Podelski. Berlin, Heidelberg : Springer, 2004. pp. 312-326 (Lecture Notes in Computer Science).

@inproceedings{d52573568d884379822b35a7ac9a689b,

title = "Lower and upper bounds in zone based abstractions of timed automata",

abstract = "Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker UPPAAL.",

keywords = "n/a OA procedure",

author = "Gerd Behrmann and Patricia Bouyer and Larsen, \{Kim G.\} and Radek Pel{\'a}nek",

year = "2004",

month = mar,

day = "29",

doi = "10.1007/b96393",

language = "English",

isbn = "978-3-540-21299-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "312--326",

editor = "Kurt Jensen and Andreas Podelski",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, TACAS ; Conference date: 29-03-2004 Through 02-04-2004",

}

Behrmann, G, Bouyer, P, Larsen, KG & Pelánek, R 2004, Lower and upper bounds in zone based abstractions of timed automata. in K Jensen & A Podelski (eds), Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2988, Springer, Berlin, Heidelberg, pp. 312-326, 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004, Barcelona, Spain, 29/03/04. https://doi.org/10.1007/b96393

Lower and upper bounds in zone based abstractions of timed automata. / Behrmann, Gerd; Bouyer, Patricia; Larsen, Kim G. et al.
Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. ed. / Kurt Jensen; Andreas Podelski. Berlin, Heidelberg: Springer, 2004. p. 312-326 (Lecture Notes in Computer Science; Vol. 2988).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Lower and upper bounds in zone based abstractions of timed automata

AU - Behrmann, Gerd

AU - Bouyer, Patricia

AU - Larsen, Kim G.

AU - Pelánek, Radek

N1 - Conference code: 10

PY - 2004/3/29

Y1 - 2004/3/29

N2 - Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker UPPAAL.

AB - Timed automata have an infinite semantics. For verification purposes, one usually uses zone based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability. We demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increases the scalability of the real-time model checker UPPAAL.

KW - n/a OA procedure

U2 - 10.1007/b96393

DO - 10.1007/b96393

M3 - Conference contribution

SN - 978-3-540-21299-7

T3 - Lecture Notes in Computer Science

SP - 312

EP - 326

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Jensen, Kurt

A2 - Podelski, Andreas

PB - Springer

CY - Berlin, Heidelberg

T2 - 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004

Y2 - 29 March 2004 through 2 April 2004

ER -

Behrmann G, Bouyer P, Larsen KG, Pelánek R. Lower and upper bounds in zone based abstractions of timed automata. In Jensen K, Podelski A, editors, Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Berlin, Heidelberg: Springer. 2004. p. 312-326. (Lecture Notes in Computer Science). doi: 10.1007/b96393

Lower and upper bounds in zone based abstractions of timed automata

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this