The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation

P.R. d' Argenio; Biniam Gebremichael

doi:10.1007/11539452_13

The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation

P.R. d' Argenio, Biniam Gebremichael

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

3 Citations (Scopus)

38 Downloads (Pure)

Abstract

Delaying the synchronization of actions may reveal some hidden behavior that would not happen if the synchronization met the specified deadlines. This precise phenomenon makes bisimulation fail to be a congruence for the parallel composition of timed automata with deadlines, a variant of timed automata where time progress is controlled by deadlines imposed on each transition. This problem has been known and unsolved for several years. In this paper we give a characterization of the coarsest congruence that is included in the bisimulation relation. In addition, a symbolic characterization of such relation is provided and shown to be decidable. We also discuss the pitfalls of existing parallel compositions in this setting and argue that our definition is both reasonable and sufficiently expressive as to consider the modeling of both soft and hard real-time constraints.

Original language	English
Title of host publication	CONCUR 2005 – Concurrency Theory
Subtitle of host publication	16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings
Editors	Martín Abadi, Luca de Alfaro
Place of Publication	Berlin
Publisher	Springer
Pages	125-140
Number of pages	16
ISBN (Electronic)	978-3-540-31934-4
ISBN (Print)	978-3-540-28309-6
DOIs	https://doi.org/10.1007/11539452_13
Publication status	Published - 2005
Event	16th International Conference on Concurrency Theory, CONCUR 2005 - San Francisco, United States Duration: 23 Aug 2005 → 26 Aug 2005 Conference number: 16

Publication series

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

Conference

Conference	16th International Conference on Concurrency Theory, CONCUR 2005
Abbreviated title	CONCUR
Country/Territory	United States
City	San Francisco
Period	23/08/05 → 26/08/05

Keywords

Parallel composition
Process algebra
Time progress
Time automaton
Small relation

Access to Document

10.1007/11539452_13

D'Argenio2005coarsestAccepted author version, 244 KB

Cite this

d' Argenio, P. R., & Gebremichael, B. (2005). The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation. In M. Abadi, & L. de Alfaro (Eds.), CONCUR 2005 – Concurrency Theory: 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings (pp. 125-140). (Lecture Notes in Computer Science; Vol. 3653). Springer. https://doi.org/10.1007/11539452_13

d' Argenio, P.R. ; Gebremichael, Biniam. / The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation. CONCUR 2005 – Concurrency Theory: 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings. editor / Martín Abadi ; Luca de Alfaro. Berlin : Springer, 2005. pp. 125-140 (Lecture Notes in Computer Science).

@inproceedings{9343991f35d04426abb26a3bd13f1de4,

title = "The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation",

abstract = "Delaying the synchronization of actions may reveal some hidden behavior that would not happen if the synchronization met the specified deadlines. This precise phenomenon makes bisimulation fail to be a congruence for the parallel composition of timed automata with deadlines, a variant of timed automata where time progress is controlled by deadlines imposed on each transition. This problem has been known and unsolved for several years. In this paper we give a characterization of the coarsest congruence that is included in the bisimulation relation. In addition, a symbolic characterization of such relation is provided and shown to be decidable. We also discuss the pitfalls of existing parallel compositions in this setting and argue that our definition is both reasonable and sufficiently expressive as to consider the modeling of both soft and hard real-time constraints.",

keywords = "Parallel composition, Process algebra, Time progress, Time automaton, Small relation",

author = "{d' Argenio}, P.R. and Biniam Gebremichael",

year = "2005",

doi = "10.1007/11539452_13",

language = "English",

isbn = "978-3-540-28309-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "125--140",

editor = "Mart{\'i}n Abadi and {de Alfaro}, Luca",

booktitle = "CONCUR 2005 – Concurrency Theory",

note = "16th International Conference on Concurrency Theory, CONCUR 2005, CONCUR ; Conference date: 23-08-2005 Through 26-08-2005",

}

d' Argenio, PR & Gebremichael, B 2005, The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation. in M Abadi & L de Alfaro (eds), CONCUR 2005 – Concurrency Theory: 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings. Lecture Notes in Computer Science, vol. 3653, Springer, Berlin, pp. 125-140, 16th International Conference on Concurrency Theory, CONCUR 2005, San Francisco, California, United States, 23/08/05. https://doi.org/10.1007/11539452_13

The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation. / d' Argenio, P.R.; Gebremichael, Biniam.
CONCUR 2005 – Concurrency Theory: 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings. ed. / Martín Abadi; Luca de Alfaro. Berlin: Springer, 2005. p. 125-140 (Lecture Notes in Computer Science; Vol. 3653).

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

TY - GEN

T1 - The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation

AU - d' Argenio, P.R.

AU - Gebremichael, Biniam

N1 - Conference code: 16

PY - 2005

Y1 - 2005

N2 - Delaying the synchronization of actions may reveal some hidden behavior that would not happen if the synchronization met the specified deadlines. This precise phenomenon makes bisimulation fail to be a congruence for the parallel composition of timed automata with deadlines, a variant of timed automata where time progress is controlled by deadlines imposed on each transition. This problem has been known and unsolved for several years. In this paper we give a characterization of the coarsest congruence that is included in the bisimulation relation. In addition, a symbolic characterization of such relation is provided and shown to be decidable. We also discuss the pitfalls of existing parallel compositions in this setting and argue that our definition is both reasonable and sufficiently expressive as to consider the modeling of both soft and hard real-time constraints.

AB - Delaying the synchronization of actions may reveal some hidden behavior that would not happen if the synchronization met the specified deadlines. This precise phenomenon makes bisimulation fail to be a congruence for the parallel composition of timed automata with deadlines, a variant of timed automata where time progress is controlled by deadlines imposed on each transition. This problem has been known and unsolved for several years. In this paper we give a characterization of the coarsest congruence that is included in the bisimulation relation. In addition, a symbolic characterization of such relation is provided and shown to be decidable. We also discuss the pitfalls of existing parallel compositions in this setting and argue that our definition is both reasonable and sufficiently expressive as to consider the modeling of both soft and hard real-time constraints.

KW - Parallel composition

KW - Process algebra

KW - Time progress

KW - Time automaton

KW - Small relation

U2 - 10.1007/11539452_13

DO - 10.1007/11539452_13

M3 - Conference contribution

SN - 978-3-540-28309-6

T3 - Lecture Notes in Computer Science

SP - 125

EP - 140

BT - CONCUR 2005 – Concurrency Theory

A2 - Abadi, Martín

A2 - de Alfaro, Luca

PB - Springer

CY - Berlin

T2 - 16th International Conference on Concurrency Theory, CONCUR 2005

Y2 - 23 August 2005 through 26 August 2005

ER -

d' Argenio PR, Gebremichael B. The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation. In Abadi M, de Alfaro L, editors, CONCUR 2005 – Concurrency Theory: 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005. Proceedings. Berlin: Springer. 2005. p. 125-140. (Lecture Notes in Computer Science). doi: 10.1007/11539452_13

The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this