A Calculus for Timed Automata (Extended Abstract)

Pedro R. D'Argenio; Ed Brinksma

doi:10.1007/3-540-61648-9_37

A Calculus for Timed Automata (Extended Abstract)

Pedro R. D'Argenio, Ed Brinksma

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

202 Downloads (Pure)

Abstract

A language for representing timed automata is introduced. Its semantics is defined in terms of timed automata. This language is complete in the sense that any timed automaton can be represented by a term in the language. We also define a direct operational semantics for the language in terms of (timed) transition systems. This is proven to be equivalent (or, more precisely, timed bisimilar) to the interpretation in terms of timed automata.

In addition, a set of axioms is given that is shown to be sound for timed bisimulation. Finally, we introduce several features including the parallel composition and derived time operations like wait, time-out and urgency. We conclude with an example and show that we can eliminate non-reachable states using algebraic techniques.

Original language	English
Title of host publication	Formal Techniques in Real-Time and Fault-Tolerant Systems
Subtitle of host publication	4th International Symposium Uppsala, Sweden, September 9–13, 1996. Proceedings
Editors	Bengt Jonsson, Joachim Parrow
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	110-129
Number of pages	20
ISBN (Electronic)	978-3-540-70653-3
ISBN (Print)	978-3-540-61648-1
DOIs	https://doi.org/10.1007/3-540-61648-9_37
Publication status	Published - 1996
Event	4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996 - Uppsala, Sweden Duration: 9 Sept 1996 → 13 Sept 1996 Conference number: 4

Publication series

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

Conference

Conference	4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996
Abbreviated title	FTRTFT
Country/Territory	Sweden
City	Uppsala
Period	9/09/96 → 13/09/96

Keywords

FMT-PA: PROCESS ALGEBRAS
FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
Parallel operator
Equational theory
Parallel composition
Process algebra
Conservative extension

Access to Document

10.1007/3-540-61648-9_37

D'Argenio1996calculusAccepted author version, 311 KB
D'Argenio1996calculusFinal published version, 1.08 MB

Cite this

D'Argenio, P. R., & Brinksma, E. (1996). A Calculus for Timed Automata (Extended Abstract). In B. Jonsson, & J. Parrow (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996. Proceedings (pp. 110-129). (Lecture Notes in Computer Science; Vol. 1135). Springer. https://doi.org/10.1007/3-540-61648-9_37

@inproceedings{e7fc8ed36bbb402e9e1eb781526bd168,

title = "A Calculus for Timed Automata (Extended Abstract)",

abstract = "A language for representing timed automata is introduced. Its semantics is defined in terms of timed automata. This language is complete in the sense that any timed automaton can be represented by a term in the language. We also define a direct operational semantics for the language in terms of (timed) transition systems. This is proven to be equivalent (or, more precisely, timed bisimilar) to the interpretation in terms of timed automata.In addition, a set of axioms is given that is shown to be sound for timed bisimulation. Finally, we introduce several features including the parallel composition and derived time operations like wait, time-out and urgency. We conclude with an example and show that we can eliminate non-reachable states using algebraic techniques.",

keywords = "FMT-PA: PROCESS ALGEBRAS, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, Parallel operator, Equational theory, Parallel composition, Process algebra, Conservative extension",

author = "D'Argenio, {Pedro R.} and Ed Brinksma",

year = "1996",

doi = "10.1007/3-540-61648-9_37",

language = "English",

isbn = "978-3-540-61648-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "110--129",

editor = "Bengt Jonsson and Joachim Parrow",

booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems",

address = "Germany",

note = "4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996, FTRTFT ; Conference date: 09-09-1996 Through 13-09-1996",

}

D'Argenio, PR & Brinksma, E 1996, A Calculus for Timed Automata (Extended Abstract). in B Jonsson & J Parrow (eds), Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996. Proceedings. Lecture Notes in Computer Science, vol. 1135, Springer, Berlin, Heidelberg, pp. 110-129, 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996, Uppsala, Sweden, 9/09/96. https://doi.org/10.1007/3-540-61648-9_37

A Calculus for Timed Automata (Extended Abstract). / D'Argenio, Pedro R.; Brinksma, Ed.
Formal Techniques in Real-Time and Fault-Tolerant Systems: 4th International Symposium Uppsala, Sweden, September 9–13, 1996. Proceedings. ed. / Bengt Jonsson; Joachim Parrow. Berlin, Heidelberg: Springer, 1996. p. 110-129 (Lecture Notes in Computer Science; Vol. 1135).

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

TY - GEN

T1 - A Calculus for Timed Automata (Extended Abstract)

AU - D'Argenio, Pedro R.

AU - Brinksma, Ed

N1 - Conference code: 4

PY - 1996

Y1 - 1996

N2 - A language for representing timed automata is introduced. Its semantics is defined in terms of timed automata. This language is complete in the sense that any timed automaton can be represented by a term in the language. We also define a direct operational semantics for the language in terms of (timed) transition systems. This is proven to be equivalent (or, more precisely, timed bisimilar) to the interpretation in terms of timed automata.In addition, a set of axioms is given that is shown to be sound for timed bisimulation. Finally, we introduce several features including the parallel composition and derived time operations like wait, time-out and urgency. We conclude with an example and show that we can eliminate non-reachable states using algebraic techniques.

AB - A language for representing timed automata is introduced. Its semantics is defined in terms of timed automata. This language is complete in the sense that any timed automaton can be represented by a term in the language. We also define a direct operational semantics for the language in terms of (timed) transition systems. This is proven to be equivalent (or, more precisely, timed bisimilar) to the interpretation in terms of timed automata.In addition, a set of axioms is given that is shown to be sound for timed bisimulation. Finally, we introduce several features including the parallel composition and derived time operations like wait, time-out and urgency. We conclude with an example and show that we can eliminate non-reachable states using algebraic techniques.

KW - FMT-PA: PROCESS ALGEBRAS

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - Parallel operator

KW - Equational theory

KW - Parallel composition

KW - Process algebra

KW - Conservative extension

U2 - 10.1007/3-540-61648-9_37

DO - 10.1007/3-540-61648-9_37

M3 - Conference contribution

SN - 978-3-540-61648-1

T3 - Lecture Notes in Computer Science

SP - 110

EP - 129

BT - Formal Techniques in Real-Time and Fault-Tolerant Systems

A2 - Jonsson, Bengt

A2 - Parrow, Joachim

PB - Springer

CY - Berlin, Heidelberg

T2 - 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 1996

Y2 - 9 September 1996 through 13 September 1996

ER -

A Calculus for Timed Automata (Extended Abstract)

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this